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
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.
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
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.
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.
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.
- Girard, Lafont and Taylor: Proofs and Types
- Harper: Practical Foundations for Programming Languages
- Pierce: Advanced Topics in Types and Programming Languages
- Normalization for Goedel's System T
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).
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:
- Non-optimizing compilation of a structured imperative language to a virtual machine, and its correctness proof.
- Notions of semantic preservation.
- A panorama of mechanized semantics: small-step, big-step, coinductive big-step, definitional interpreter, denotational semantics.
- Examples of program optimizations: dead code elimination, register allocation.
- Design and soundness proof of a generic static analyzer based on abstract interpretation.
- Compiler verification "in the large" : an overview of the CompCert verified C compiler.
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:
- Benjamin Pierce et al. Software Foundations.
- Hervé Grall and Xavier Leroy. Coinductive big-step operational semantics.
- Xavier Leroy. A formally verified compiler back-end.
- Yves Bertot. Structural abstract interpretation, A formal study using Coq.
- Patrick Cousot. MIT Course 16.399: Abstract Interpretation.
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.
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:
- Hoare type theory (HTT) and comparison to alternative approaches.
- Realizing HTT in Coq through the Ynot libraries.
- Separation logic and its role in reasoning about (higher-order) imperative programs.
- Tactics for simplifying separation-style goals and automating proofs of (partial) correctness.
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.
- Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176-210, 405-431, 1935. English translation in M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68-131, North-Holland, 1969. Basic historical reference; introduces both the natural deduction and the sequent calculus.
- Dag Prawitz. Natural Deduction. Almquist & Wiksell, Stockholm, 1965. Investigates the metatheory of natural deduction.
- W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479-490. Academic Press, 1980. Hitherto unpublished note of 1969, rearranged, corrected, and annotated by Howard. The note introducing the Curry-Howard isomorphism for natural deduction. Curry had previously described it for combinatory logic.
- Per Martin-Löf. On the meanings of the logical constants and the justifications of the logical laws. Technical report, Scuola di Specializzazione in Logica Matematica, Dipartimento di Matematica, Università di Siena, April 1983. Reprinted in the Nordic Journal of Philosophical Logic 1(1), pp. 11-60, 1996. [Available electronically] Lays out the justification of the definition of the logical connectives by distinguishing judgments from propositions.
- Michael Dummett. The Logical Basis of Metaphysics. Harvard University Press, Cambridge, Massachusetts, 1991. The William James Lectures, 1976. Analysis of verificationists and pragmatist points of view and their harmony.
- Frank Pfenning and André Platzer. Modal logic. Notes for a course at Carnegie Mellon University, Spring 2010. Lectures 1, 2, 8. [Available electronically] Lectures notes closely related to lectures 1-3 presented at the summer school.
- Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11:511-540, 2001. Notes to an invited talk at the Workshop on Intuitionistic Modal Logics and Applications (IMLA'99), Trento, Italy, July 1999. [PDF] Introduces explicit notions of local soundness and completeness and applies them in the richer setting of modal logic where additional judgments arise.
- Frank Pfenning. Structural cut elimination I. Intuitionistic and classical logic. Information and Computation, 157(1/2):84-141, March 2000. [PDF] Introduces the cut elimination proof of lecture 3 and its formalization in a logical framework.
- Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):197-347, 1992. The seminal paper on focusing, treating classical linear logic.
- Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, November 2009. [PDF] A paper that also treats polarization and intuitionistic logic. Probably the closest reference for Lecture 4.
- Sean McLaughlin and Frank Pfenning. Efficient intuitionistic theorem proving with the polarized inverse method. In R.A.Schmidt, editor, Proceedings of the 22nd International Conference on Automated Deduction (CADE-22), pages 230-244, Montreal, Canada, August 2009. Springer LNCS 5663. [PDF] An application of focusing in a realistic theorem prover.
- Noam Zeilberger. The Logical Basis of Evaluation Order and Pattern-Matching. PhD thesis, Department of Computer Science, Carnegie Mellon University, May 2009. Available as Technical Report CMU-CS-09-122. An application of focusing in the design of programming languages.
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:
- Proving properties of functional programs on numbers and lists.
- Inductive data, propositions, and proofs.
- Definition of logical connectives and quantifiers.
- Essential proof tactics and basic automation.
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.
Plenary Lectures
Coq Labs — Brent Yorgey
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?
Formal Verification in Industry — John Harrison
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.