Oregon Programming Languages Summer School

Types, Logic, Semantics, and Verification

University of Oregon — Eugene OR

June 15-27, 2015

Sponsors:

June 15-27, 2015

Types, Logic, Semantics, and Verification

Preparation

Prior to OPLSS, students should have the following software ready on their laptops

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

  1. Intuitionistic logic. Natural deduction, harmony of introductions and eliminations, relation to classical logic.
  2. Proofs as programs. Proof term assignment, Curry-Howard isomorphism, subject reduction, type checking.
  3. Proof search and sequent calculus. Identity and cut, left and right rules, cut elimination.
  4. 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.1-5)
Lecture 4 video1 | video2 | video3 | video4 | notes (pages L8.5-13) | 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 Martin-Lö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 Martin-Lö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 first-order 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 Notes

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 Inductive-Recursive Definitions in Intuitionistic Type Theory — Peter Dybjer

Building on the lectures by Robert Harper we will further explore Martin-Löf's intuitionistic type theory. This is a theory of inductive and inductive-recursive 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 well-founded 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 Programming-Language Semantics — Adam Chlipala

An introduction to the Coq software for building machine-checked mathematical proofs, building on the type-theory 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 hands-on sessions, students will be encouraged both to apply these formalisms to concrete programs and to extend the formalisms to handle new programming-language 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 simply-typed lambda calculus (STLC). We will then add recursive types to STLC and develop a step-indexed logical relation, using step-indexing to ensure that the logical relation remains well-founded. 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

Mark Bickford

Lecture 1 video1 | video2 | video3 | video4 | video5 | video6
Lecture 2 video1 | video2 | video3 | video4 | video5

Robert Constable

Lecture 1 video1 | video2 | video3
Lecture 2 video1 | video2 | video3 | video4 | video5 | notes

Low-res copies of videos hosted on Youtube

© University of Oregon Department of Computer and Information Science, 1202 University of Oregon, Eugene OR 97403-1202