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 PaulinMohring
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 manyusability 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
