University of Oregon

10th Annual Oregon Programming Languages Summer School — June 16-July 1, 2011

Types, Semantics and Verification

Lecture Schedule

The program consists of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research. This year, on the occasion of the tenth anniversary of the summer school, two plenary lectures will complement the technical program.

Some of the lectures will assume interactive sessions using Coq, a proof assistant. Students are encouraged to bring a laptop on which coq has been installed, and to form small working groups during the interactive sessions. Moreover, some Coq-labs will be offered in order to give the participants the opportunity to gain more practice in using Coq. The Coq labs will be directed by Brent Yorgey from University of Pennsylvania. Coq is available from INRIA.

Technical Lectures

Logical Relations — Amal Ahmed

  1. video
  2. video
  3. video
  4. video
  5. video
  6. video
  7. video
  8. video
  9. video
  10. video
  11. video

Software Verification — Andrew Appel

To build verified software, write your programs in a language with a tractable proof theory, embedded in a proof assistant that can manipulate programs and proofs. One such language is Gallina, the pure functional programming language embedded in Coq. I'll teach a hands-on lab course in Coq, on writing functional programs and proving them correct. (Prerequisite: Pierce's lectures and homeworks in this summer school.) In addition, I may devote a lecture to a completely different domain of software: imperative programs with proofs in higher-order concurrent separation logic.

  1. video
  2. video
  3. video
  4. video
  5. video

Monadic Effects — Nick Benton

Computational monads were introduced by Moggi as a way of structuring the denotational semantics of languages with side effects and have been extensively used, studied and generalized by researchers in logic and semantics. By a pleasing interplay of theory and practice, monads (both generally and in particular) have also become widespread as a program structuring device, most notably as a way of integrating side effects in "pure" functional languages. These lectures will cover computational monads and some of their close relations, such as arrows and effect systems, from the perspectives of logic and semantics, programming and compiler implementation. Advanced topics will include Filinski-style monadic reflection and the algebraic approach to effects introduced by Plotkin and Power.

Lectures 1&2 Notes | Lectures 3 Notes | Lectures 4 Notes | Lectures 5 Notes

  1. video
  2. video
  3. video
  4. video
  5. video
  6. video
  7. video
  8. video
  9. video
  10. video
  11. video
  12. video

Polymorphic Logic — Robert Constable

Various theorems about program control structure can be expressed polymorphically in programming logics, and these results shed light on ways to obtain more efficient program extracts from formal constructive proofs. This lecture examines some of these theorems and their applications, including one whose extract is the Y combinator. In addition we examine some new metamathematical results about polymorphic logics.

  1. video
  2. video
  3. video
  4. video
  5. video

Polarisation and Focusing — Pierre-Louis Curien

Polarisation and focusing have appeared in the early nineties in the context of proof search in the setting of linear logic (Andreoli), and closely after as a basis to Girard's constructive analysis of classical logic (system LC). The focusing restriction on proofs is both mild enough to catch classical provability and strong enough to cure the intrinsic non-confluence of classical cut-elimination. Polarisation has a nice computational interpretation, where positive and negative connectives match eager and lazy data types, respectively. The syntax of Curien and Herbelin for the duality of computation (2000) can be adapted to the polarised setting, leading to focalising system L (proposed shortly before 2010, in two variants, first by Munch-Maccagnoni, and then by Curien and Munch-Maccagnoni). We advocate this system, and more generally the "systems L" based on Curien-Herbelin's syntactic kit, as intermediate languages for the study and the proofs of correction of abstract machines. We shall also discuss the relations of focalising systeml L with CPS translations, and with linear logic.

  1. video
  2. video
  3. video
  4. video
  5. video
  6. video
  7. video

Type Theory Foundation — Robert Harper

The method of logical relations is a fundamental tool in type theory that is used to prove termination and normalization and to analyze equations between terms, including parametricity properties for polymorphism. The main idea is to interpret types as relations (of a suitable class) on terms by associating to each type constructor a "relational action" that determines the relation associated to a compound type as a function of its constituent types. The interpretation is chosen so that well-typed terms stand in the relation associated to their type, and so that related terms satisfy a property of interest, from which it follows that well-typed terms have that property. The method has many applications, but all share the characteristic that a global property of terms is reduced to local properties of types. I will develop the theory of logical relations from first principles, concentrating on two important cases, Goedel's System T and Girard's System F.

  1. video
  2. video
  3. video
  4. video
  5. video
  6. video
  7. video
  8. video
  9. video
  10. video
  11. video

The Calculus of Inductive Constructions — Hugo Herbelin

Coq is based on the formalism of the Calculus of Inductive Constructions (CIC) which is both a logic and a programming language. As is emphasized in previous lectures, the CIC builds on a pure type system with higher-order polymorphism and stratified type universes by incorporating the inductive types from Martin-Lof's type theory and their coinductive variants.

The lectures will first focus on a reconstruction of CIC from its syntactic components (lambda-calculus, recursion and corecursion, weak and strong dependent pattern-matching, types, sorts, conversion rule) and their expressivity (higher-order logic, Leibniz equality, Pi-types, base types, W-types and set-theoretic universes). They will then focus on CIC's models (logical relations for justifying normalization, set-theoretic models for justifying the consistency of extra axioms). The lectures will conclude with an investigation of advanced issues for CIC (classical logic, proof-irrelevance, axiom of choice and extensional equality).

  1. video
  2. video
  3. video
  4. video
  5. video
  6. video
  7. video
  8. video
  9. video
  10. video

Compiler Certification — Xavier Leroy

Formal semantics of programming languages supports not only reasoning over individual programs (program correctness), but also reasoning over program transformations and static analyses, as typically found in compilers (tool correctness). With the help of a proof assistant, we can prove semantic preservation properties of program transformations and semantic soundness properties of static analyses that greatly increase the confidence we can have in compilers and program verification tools.

The topics covered in this lecture include:

We will use the Coq proof assistant and build on the formalization of the IMP language shown in Benjamin Pierce's "Software Foundations" lectures.

Course material available here, especially the corresponding Coq development (compiler-verification.tar.gz).

References:

  1. video
  2. video
  3. video
  4. video
  5. video
  6. video
  7. video
  8. video
  9. video
  10. video
  11. video
  12. video
  13. video
  14. video
  15. video

Programming languages in string diagrams — Paul-André Melliès

String diagrams were introduced by Roger Penrose in the early 1970s as a graphical way to depict computations arising in differential geometry and theoretical physics. The purpose of the course is to show how these string diagrams can be used as a unifying framework for various areas of logic and programming language semantics. In particular, we will treat applications to concurrency theory, game semantics and computational effects. The course may be understood as a foundational approach to side effects in resource-aware programming languages, and their relationship to dependent types.

Lecture 1. String diagrams in monoidal categories. Monoidal categories, string diagrams, functorial boxes, categorical semantics of resource modalities, recursion as a fixpoint operator, trace operators.

Lecture 2. Game semantics in string diagrams. Linear continuations, game semantics, ribbon categories, dialogue categories, tensorial logic, polarization and the chirality principle, focusing as a turn policy, adjunctions in 2-categories, tensorial proof nets, correctness criterion.

Lecture 3. Categorical semantics of side effects. Computational monads, premonoidal categories, categorical actions, linear effect systems, application to the global and the local state monad.

Lecture 4. Local stores in string diagrams. Finitary monads, algebraic theories, monoids and mnemoids, presheaf categories, monads with arities, graded algebraic theories, local stores in string diagrams.

Lecture Materials

  1. video
  2. video
  3. video
  4. video
  5. video
  6. video

Imperative Programming in Coq — Greg Morrisett

Next-generation programming languages are attempting to integrate more expressive forms of types (e.g., dependent and refinement types). But the attempts at taking standard languages, like Java, ML, Haskell, etc. and extending them with dependency and refinement run up against a host of problems: unsoundness due to side-effects, incompleteness due to weak logics, and absence of modularity due to a lack of appropriate abstraction mechanisms.

An alternative is to start with Coq's (very) pure, functional core language (Gallina) and augment it with features needed to do practical programming. In particular, we will consider extensions to Gallina that support higher-order programs with side-effects, and how to smoothly integrate specifications of those effects into types so that we get a modular treatment of programs with dependency and refinement.

Our expected topics of discussion will include:

Building upon the earlier presentations in the Summer School, students will learn how to use Coq to build and prove correct simple imperative data structures (e.g., linked-lists, hash-tables, etc.) and algorithms (e.g., unificaton).

Online Materials

  1. video
  2. video
  3. video
  4. video
  5. video
  6. video
  7. video

Proof Theory Foundation — Frank Pfenning

Lecture 1: Intuitionistic logic.
Natural deduction, verifications and uses, harmony of introduction and eliminations, difference from classical logic.
Lecture 2: Proofs as programs.
Proof term assignment, Curry-Howard isomorphism, subject reduction, notions of normal form, type checking.
Lecture Notes on bidirectional typechecking
Lecture 3: Proof search and sequent calculus.
Sequent calculus as search calculus, left and right rules, identity, cut elimination, connection to natural deduction.
Lecture 4: Focusing.
Weak focusing, cut elimination revisited, inversion, full focusing, proof terms and pattern matching, logic programming.

Below are some basic references. Most closely related to the material in lectures 1-3 (although not in the same order) are Lecture 1: Judgments and Propositions, Lecture 2: Proofs as Programs and Lecture 8: Sequent Calculus from a course on Modal Logic at Carnegie Mellon in Spring 2010. Attached below are lectures notes for Lecture 4: Focusing.

  1. video
  2. video
  3. video
  4. video

Proof Theory in Coq — Benjamin Pierce

Coq is a mechanized proof assistant that is widely used for reasoning about programs, programming languages, and programming tools. While it enjoys a very simple foundational core based on type theory, the full Coq system is rich and complex, and can be daunting for beginners. These lectures will give a pragmatic introduction to the essential features of Coq and their use in formalizing the theory of programming languages, based on the first part of the textbook Software Foundations in Coq (Pierce et al.). They will be complemented with plenty of hands-on exercises.

Lecture topics will include:

  1. video
  2. video
  3. video
  4. video
  5. video
  6. video
  7. video
  8. video
  9. video
  10. video

Semilattices, Domains, and Computability — Dana Scott

One popular notion of a (Scott-Ersov) domain is defined as a bounded complete algebraic cpo. Such an abstract a definition is not always so helpful for beginners. The speaker found recently that there is an easy-to-construct domain of countable semilattices giving isomorphic copies of all countably based domains. This approach seems to have advantages over both the so-called "information systems" and the more abstract lattice/ topological definitions, and it makes the finding of solutions to domain equations and models for the lambda-calculus very elementary to justify. The "domain of domains" also has a natural computable structure in this formulation. Built on top of this construction is a modeling of Martin-Löf type theory.

Notes 1 | Notes 2

  1. video
  2. video
  3. video
  4. video
  5. video

Plenary Lectures

Coq Labs — Brent Yorgey

Exercises

What is a Proof? — Some Challenges for Automated Theorem Proving — Dana Scott

Once in a while I find a theorem that is "self-proving" in the sense that, having stated the needed definitions, the information in the hypotheses to the theorem somehow expands into what is required to establish the conclusion. Life is not always so easy, however. In the talk, proofs of several fairly simple theorems will be presented where the proof seems to depend on ADDED STRUCTURE. The question is: How we could guide a (semi) automated system to uncover such crucial structure?

Notes

  1. video
  2. video

Formal Verification in Industry — John Harrison

  1. video
  2. video
  3. video
  4. video

Design Issues for Implemented Type Theories — Robert Constable

Significant theoretical differences among the major implemented type theories are based on design goals informed by metamathematical theorems and the results in the semantic theory of programming languages. These goals and design decisions are not often compared and analyzed in the literature. I will undertake such comparisons in this lecture, focusing on differences between Computational Type Theory (CTT), implemented in Nuprl and MetaPrl, and the Calculus of Inductive Constructions (CIC) implemented in Coq. Both theories are constructive and both use the LCF tactic mechanism for automation, but initial differences in goals have led to interesting practical consequences, some unexpected.

  1. video
  2. video
  3. video
  4. video

Sponsors
Copyright © University of Oregon Department of Computer and Information Science. All rights reserved.
Privacy Policy