Preparation
Prior to OPLSS, students should have the following software ready on their laptops Coq 8.5 or later
 GHC 7.8 or later
 Cabal 1.18 or later (the Haskell Platform includes GHC and Cabal)
 Agda 2.4 or later
 OCaml 4.02 or later with OPAM 1.2 or later
 Sill 1.3 or later;
if OPAM is installed, sill can be installed with
opam install sill
 Proof General
Technical Lectures
The program consists of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.
Basic Proof Theory — Frank Pfenning
 Intuitionistic logic. Natural deduction, harmony of introductions and eliminations, relation to classical logic.
 Proofs as programs. Proof term assignment, CurryHoward isomorphism, subject reduction, type checking.
 Proof search and sequent calculus. Identity and cut, left and right rules, cut elimination.
 Linear logic. Sequent calculus revisited, cut reduction as concurrent computation, connectives of linear logic.

 Polarization and focusing. Weak focusing, inversion, logic programming.
 or Concurrent programming in linear logic.
Lecture 1
video1 
video2 
video3 
video4 
notes
Lecture 2
video1 
video2 
video3 
video4 
notes
Lecture 3
video1 
video2 
video3 
video4 
notes (pages L8.15)
Lecture 4
video1 
video2 
video3 
video4 
notes (pages L8.513) 
student notes
Lecture 5
video1 
video2 
video3 
video4 
notes 1 
notes 2 
notes 3 
student notes 1 
student notes 2
Introduction to Dependent Type Theory — Robert Harper
This series of lectures will introduce the audience to the fundamentals of intuitionistic type theory. Several variations will be considered, starting with MartinLöf's type theory, in extensional and intensional form, and extending to higher type theory. The lectures complement those of Frank Pfenning and Ed Morehouse, who will be lecturing on proof theory and category theory, respectively (the latter with emphasis on categorial logic). These lectures will provide the theoretical foundation for the application of the Coq Theorem Prover by other lecturers, including Adam Chlipala. They will also serve as a reference point for Robert Constable's lectures on computational type theory, the language of the NuPRL Proof Development System, a rather different approach to type theory that, unlike MartinLöf's type theory, is based directly on a computational foundation.
Lecture 1
video1 
video2 
video3 
video4
Lecture 2
video1 
video2 
video3 
video4 
video5
Lecture 3
video1 
video2 
video3 
video4 
video5
Lecture 4
video1 
video2 
video3 
video4 
video5 
student notes
Lecture 5
video1 
video2 
video3 
video4 
video5 
video6 
student notes
Basic Category Theory: Semantics of Proof Theory — Ed Morehouse
This lecture series will introduce students to category theory through the lens of categorical semantics for the proof theory presented in the parallel lectures, "Basic Proof Theory".
Topics covered will include universal constructions, duality, functoriality, naturality, adjunctions and the interpretation of logical theories in categories. In the process, we will discover the features needed to give a sound and complete categorical semantics for intuitionistic firstorder proof theory.
In addition to introducing students to basic categorical tools and techniques, a goal of these lectures will be to offer an alternative, algebraic, perspective on proof theory. Throughout, we will emphasize the benefits of behavioral (versus structural) characterizations, and of diagrammatic reasoning.
Lecture 1
video1 
video2 
video3 
video4
Lecture 2
video1 
video2 
video3 
video4
Lecture 3
video1 
video2 
video3 
video4 
video5
Lecture 4
video1 
video2 
video3 
video4 
student notes
Lecture 5
video1 
video2 
video3 
video4 
video5
Inductive and InductiveRecursive Definitions in Intuitionistic Type Theory — Peter Dybjer
Building on the lectures by Robert Harper we will further explore MartinLöf's intuitionistic type theory. This is a theory of inductive and inductiverecursive definitions based on a lambda calculus with dependent types. The "sets" of the theory are inductively defined data types which are similar to the data types available in ordinary functional programming languages, except that the elements are all wellfounded structures. We will also show how the data types in intuitionistic type theory can be implemented in the dependently typed programming language Agda. Although Agda is based on intuitionistic type theory, it contains a number of extensions which make it more practical to use as a real alternative to ordinary functional programming languages.
References
Lecture 1
video1 
video2 
video3 
video4 
Exercises

Web Resources

LF

IType

MLTT
Lecture 2
video1 
video2 
video3 
video4
Lecture 3
video1 
video2 
video3 
video4
Lecture 4
video1 
video2 
video3 
video4
Lecture 5
video1 
video2 
video3 
video4
The Coq Proof Assistant and Its Applications to ProgrammingLanguage Semantics — Adam Chlipala
An introduction to the Coq software for building machinechecked mathematical proofs, building on the typetheory foundations introduced in Robert Harper's lectures, and complementing Peter Dybjer's lectures on Agda, a programming language built on a similar foundation. We'll start by looking at proving correctness of functional programs, via induction and equational reasoning; and then move on to proofs about inductively defined relations, applied specifically to modeling programs as state transition systems. These ingredients prepare us to reason about operational semantics, the core of most approaches today to rigorous proof about program behavior. The lecture series wraps up with examples of two influential approaches to doing mostly automatic proof of program safety: sound type systems for functional programs and Hoare logic for imperative programs. In the handson sessions, students will be encouraged both to apply these formalisms to concrete programs and to extend the formalisms to handle new programminglanguage features.
Lecture 1
video1 
video2 
video3 
video4
Lecture 2
video1 
video2 
video3 
video4
Lecture 3
video1 
video2 
video3 
video4
Lecture 4
video1 
video2 
video3 
video4
Lecture 5
video1 
video2 
video3 
video4
Lecture 6
video1 
video2 
video3 
video4
Logical Relations — Amal Ahmed
These lectures will introduce students to the proof method of logical relations. Logical relations have been used to prove a wide range of properties, including normalization, type safety, equivalence of programs, noninterference (in security typed languages), and compiler correctness. We will start by looking at how to prove normalization and type safety for the simplytyped lambda calculus (STLC). We will then add recursive types to STLC and develop a stepindexed logical relation, using stepindexing to ensure that the logical relation remains wellfounded. We will cover polymorphic and existential types and develop a logical relation to reason about the associated notions of parametricity and representation independence. The lectures will also discuss how to establish that a logical relation corresponds to contextual equivalence. The lecture series will conclude with a brief look at past and future applications of logical relations, particularly in the realm of compositional compiler correctness.
Lecture 1
video1 
video2 
video3 
video4 
video5
Lecture 2
video1 
video2 
video3 
video4 
video5 
student notes 1 
student notes 2 
student notes 3 
student notes 4
Lecture 3
video1 
video2 
video3 
video4
Lecture 4
video1 
video2 
video3 
video4
Lecture 5
video1 
video2 
video3 
video4 
video5 
slides
Lecture 1
video1 
video2 
video3 
video4 
video5 
video6
Lecture 2
video1 
video2 
video3 
video4 
video5
Lecture 1
video1 
video2 
video3
Lecture 2
video1 
video2 
video3 
video4 
video5 
notes