University of Oregon 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 This page is the property of the University of Oregon