Session types are a type system used to ensure correctness in concurrent programs. They guarantee that messages sent and received between concurrent programs are in the expected order and of the expected type. Session type systems have been adapted for both channel and actor systems, and are used to ensure desirable properties such as absence of communication errors or deadlocks, and protocol conformance.
Carnegie Mellon University
Fall 2021
This undergraduate course introduces students to constructive logics such as intuitionistic and linear logic, focusing on their use in computer science. The goal is to understand the distinction between classical and constructive logic, define logical connectives, implement theorem provers, and explore computational interpretations of logics. Concepts covered include natural deduction, sequent calculus, logic programming, linear logic, and many more.
No concepts data
+ 35 more concepts