Program - Background

Type Theory and its Logical Interpretation
Type theory provides a unified foundation for constructive mathematics and computer programming. These four lectures will provide an introduction to type theory from the viewpoint of constructive logic. We will consider systems of natural deduction, sequent calculus, term assignment, normalization, and operational interpretations of proof terms. The course will be based on the first half of the course Constructive Logic at Carnegie Mellon.
Lecture 1 Video | Lecture 2 Video
Lecture 3 Video | Lecture 4 Video
Lecture 5 Video | Lecture 6 Video
Lecture 7 Video
Robert Harper

Inductive Types
We introduce inductive types, which allow for a natural description of most of the data structures used in both computer science and logic, such as inductive sets à la ML (e.g. trees, lists, natural numbers). Besides the syntactic aspect of inductive definitions, is the computation part, recursion, and the logical part, induction. The expressivity of the different recursion and induction principles will be discussed. Definitions by induction are also convenient to define logical properties as least predicates satisfying some closure properties.
Lecture Notes
Lecture 1 Video Lecture 2 Video
Lecture 3 Video
Christine Paulin-Mohring

Coinductive Types and Bisimulation
We present the foundation of coinduction and bisimulation as important tools for reasoning about unbounded structures, such as, lazy streams and their equivalence.
Lecture Notes
Lecture 1 Video | Lecture 2 Video
Lecture 3 Video | Lecture 4 Video
Roy L. Crole

Linear Logic
Linear logic decomposes the usual notion of a connective in a purely connective part and a part allowing the many-usability of a formula. This provides a good tool for analyzing logic. Some of the current approaches to security are based on linear logic.
Lecture Notes
Vincent Danos