Lecture Schedule
The program consisted of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.
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. Coq is available from INRIA.
Lecture Abstracts
Type Theory Foundations — 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 welltyped terms stand in the relation associated to their type, and so that related terms satisfy a property of interest, from which it follows that welltyped 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
Proof Theory Foundations — 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, CurryHoward isomorphism, subject reduction,
notions of normal form, type checking.
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.
Intuitionistic proofs correspond to functional programs and vice versa. Since the celebrated discovery of this CurryHoward isomorphism, similar relationships have guided our understanding of advanced programming language constructs, for example, for distributed computation or staged computation. Every computer scientist should therefore understand the basic structure of proofs and their computational interpretation.
In this course we explore the theory of proofs, emphasizing the fundamental principles that underly systems of logical inference. A student taking this course will learn
 how to define and justify logical systems from first principles
 how to assess the intrinsic coherence of a logic
 how to uncover the computational meaning of proofs
 how to construct effective systems of proof search
The course is divided into four lectures.
 Natural Deduction: how to define logics
 Verifications: the intrinisic meaning of propositions
 Sequent Calculus: searching for proofs
 Focusing: from myopic to prescient inference
 Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176210, 405431, 1935. English translation in M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68131, NorthHolland, 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 formulaeastypes 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 479490. Academic Press, 1980. Hitherto unpublished note of 1969, rearranged, corrected, and annotated by Howard. The note introducing the CurryHoward isomorphism for natural deduction. Curry had previously described it for combinatory logic.
 Per MartinLö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. 1160, 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 13 presented at the summer school.
 Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11:511540, 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):84141, March 2000. [PDF] Introduces the cut elimination proof of lecture 3 and its formalization in a logical framework.
 JeanMarc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):197347, 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):47474768, 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 (CADE22), pages 230244, 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 PatternMatching. PhD thesis, Department of Computer Science, Carnegie Mellon University, May 2009. Available as Technical Report CMUCS09122. An application of focusing in the design of programming languages.
 The vector and matrix part of the lecture.
 The filing monad demo.
 Just to show that the filing monad makes you check.
 Applicative programming with effects (McBride, Paterson)
 The essence of the ITERATOR pattern (Gibbons, Oliveira)
 The starting configuration of the file, so you can try to redo the lecture yourself!
 My crib for the finished product.
 Nonoptimizing compilation of a structured imperative language to a virtual machine, and its correctness proof.
 Notions of semantic preservation.
 A panorama of mechanized semantics: smallstep, bigstep, coinductive bigstep, 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.
 Benjamin Pierce et al. Software Foundations.
 Hervé Grall and Xavier Leroy. Coinductive bigstep operational semantics.
 Xavier Leroy. A formally verified compiler backend.
 Yves Bertot. Structural abstract interpretation, A formal study using Coq.
 Patrick Cousot. MIT Course 16.399: Abstract Interpretation.
 Learn how to write and reason about imperative ADTs and programs in the context of Coq.
 Learn about and be able to apply the ideas behind separation logic for reasoning about pointers.
 Learn about an approach to tacticbased theorem proving in Coq that leads to smaller and more maintainable proof scripts.
 Build a certified type inference engine.
 A. Nanevski et al. Abstract Predicates and Mutable ADTs in Hoare Type Theory. ESOP'07.
 A. Nanevski et al. Hoare Type Theory, Polymorphism and Separation. ICFP'06.
 A. Nanevski et al. Ynot: Reasoning with the Awkward Squad ICFP'08.
 A. Chlipala et al. Effective Interactive Proofs for HigherOrder Imperative Programs. ICFP'09.
 C.McBride. Firstorder unification by structural recursion. JFP 13(6).
 A. Chlipala. Certified Programming with Dependent Types. (Draft book)
 Lecture 1 Video  pdf
 Lecture 2 Video  coqdoc  coq source
 Lecture 3 Video  coqdoc  coq source
 Lecture 4 Video  pdf
 Proving properties of functional programs on numbers and lists.
 Inductive data, propositions, and proofs.
 Definition of logical connectives and quantifiers.

Basics.v
 ESSENTIALS:
 all 1 star exercises
 andb_true_elim2
 beq_nat_refl
 more_exercises (ble_nat,refl, zero_nbeq_S, etc. )
 decreasing
 STRONGLY RECOMMENDED:
 mult_comm
 binary
 ESSENTIALS:

Lists.v
 ESSENTIALS:
 1 star exercises
 list_exercises
 list_design
 beq_natlist
 apply_exercises
 STRONGLY RECOMMENDED:
 alternate
 bag_functions
 bag_theorem
 bag_count_sum
 ESSENTIALS:

Poly.v
 ESSENTIALS:
 all 1 star exercises
 map_rev
 override_neq
 beq_nat_eq'
 plus_n_n_injective
 override_same
 beq_nat_trans
 STRONGLY RECOMMENDED:
 combine_split (and a suitable inverse)
 override_permute
 ESSENTIALS:

Ind.v
 ESSENTIALS:
 All 1 star exercises
 Give tactic proof AND proof object that if n is even, then so is 4+n.
 double_even
 ev_sum
 MyProp_0
 MyProp_plustwo
 ev_MyProp
 STRONGLY RECOMMENDED:
 ev_ev_even
 gen_dep_practice
 palindrome
 ESSENTIALS:

Logic.v
 ESSENTIALS:
 All 1 star exercises
 even_ev
 definition of True as an inductive Prop
 not_eq_beq_false
 dist_exists_or
 R_provability
 le_exercises (at least some of them)
 STRONGLY RECOMMENDED:
 MyProp_iff_ev
 R_fact
 no_repeats
 ESSENTIALS:
Below are some basic references. Most closely related to the material in lectures 13 (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.
Dependently Typed Programming — Conor McBride
In these lectures, we shall look at dependent types without the mediating lens of the CurryHoward isomorphism. We shally exploit them for data and for programs as a kind of "logical infrastructure" capturing relative notions of intrinsic validity, in contrast (but not conflict) with the use of dependent types as "logical superstructure", expressing propositions about simply typed things.
We shall explore the tradeoffs involved in working with sets indexed by data expressing size, bounds, type, and other properties which refine what it means for data to be valid. Similarly, we shall index control structures, modelling interaction relative to the state of an uncertain world.
We shall investigate the mathematical foundations of indexed data and control, with the intention of reflecting them. By manipulating types "in software", we shall begin to find tools which help us navigate the design space of indexing disciplines and negotiate our own compromise between intrinsic validity and extrinsic verification.
Lecture 1
This is basically a magic show, more about sketching the
possibilities which advanced type systems open, than about
communicating technical material. At the same time, it's a
demo of the
Strathclyde
Haskell Enhancement. If you have Haskell (and cabal), you can try
this kit with cabal install she
.
The slides are here, now that I've photographed them.
Further reading:
Lecture 2
Agda basics: some vectors, at a less crazy pace; some examples of improved hygiene; views; simply typed lambda calculus.
Humourless Marxism alert: there's quite a lot of boilerplate here. Hopefully, on Friday, we'll see the method in this madness.
Further reading:
Lecture 3
...was the back end of lecture 2.
Lecture 4
Universes, Ornaments, Algebras is based on my unfinshed draft Ornamental Algebras, Algebraic Ornaments. It's an exploration of incremental design of datatypes.
ProofsasProcesses: Reasoning about Concurrency in Computational Type Theory — Robert Constable
The Internet is changing how we work and how we think. It is based on an asynchronous message passing computing model whose services are provided by interacting protocols. Many of the critical protocols are relatively small, a dozen or so lines of code that are very difficult to comprehend and very easy to "get wrong". Many of the critical protocols are accompanied by proofs, but the level of detail required to handle the routine parts obscures the important insights.
To understand these protocols and prove their properties requires that we reason at high levels of abstraction, at the level of processes and above. Our goal is to raise the abstraction level high enough that we see processes as realizers for declarative statements about the Internet computing model in the same way that in the proofsasprograms paradigm we see programs as realizers for assertions about sequential computing.
It turns out that Computational Type Theory (CTT) is a very good host for a combined semantics of processes and programs and for a logic of events based on them. These lectures will introduce the basic ideas from CTT, a theory similar to the Calculus of Inductive Constructions (CIC). CTT is implemented in the Nuprl and MetaPRL provers and CIC is implemented in the Coq prover. The four lectures will have these titles. Computational Type Theory Basics, Processes and Systems in CTT, The Power of Automation, Game Changing Applications.
Programming Language Methods for Compositional Security — Anupam Datta
Compositional security is a recognized central scientific challenge for trustworthy computing. Contemporary systems are built up from smaller components. However, even if each component is secure in isolation, the composed system may not achieve the desired endtoend security property: an adversary may exploit complex interactions between components to compromise security. Such attacks have shown up in the wild in many different settings, including web browsers and infrastructure, network protocols and infrastructure, and application and systems software. These lectures will report on progress on applying programming language methods to address this problem and will be divided into two parts:
Part I: Protocol Composition Logic
Protocol Composition Logic (PCL) is a logic for proving security
properties of network protocols that use public and symmetric key
cryptography. The logic is designed around a process calculus with actions
for possible protocol steps including generating new random numbers,
sending and receiving messages, and performing decryption and digital
signature verifcation actions. The proof system consists of axioms about
individual protocol actions and inference rules that yield assertions
about protocols composed of multiple steps. Although assertions are
written only using the steps of the protocol, the logic is sound in a
strong sense: each provable assertion involving a sequence of actions
holds in any protocol run containing the given actions and arbitrary
additional actions by a malicious adversary. This approach lets us prove
security properties of protocols under attack while reasoning only about
the actions of honest parties in the protocol. PCL supports compositional
reasoning about complex security protocols and has been applied to a
number of industry standards including SSL/TLS, IEEE 802.11i and Kerberos V5.
Part II: Logic of Secure Systems
We present a formal framework for compositional reasoning about secure
systems. A key insight is to view a trusted system in terms of the
interfaces that the various components expose: larger trusted components
are built by combining interface calls in known ways; the adversary is
confined to the interfaces it has access to, but may combine interface
calls without restriction. Compositional reasoning for such systems is
based on an extension of relyguarantee reasoning for system correctness
to a setting that involves an adversary whose exact program is not known.
It generalizes prior work on Protocol Composition Logic. At a technical
level, the approach is based on an expressve concurrent programming
language with recursive functions for modeling interfaces and a logic of programs in
which compositional reasoning principles are formalized and proved sound
with respect to trace semantics. The methods are applied to representative
examples of webbased systems and network protocols. As a running example,
we consider an example mashup system and present a modular proof of
integrity in the presence of a class of interfaceconfined adversaries. We
also demonstrate the generality of our methods by presenting a modular
proof of symmetric key Kerberos V5 in the presence of a symbolic adversary.
References:

A. Datta,
A. Derek,
J. C. Mitchell,
A. Roy,
Protocol Composition Logic (PCL),
in
Electronic Notes in Theoretical Computer Science (Gordon D. Plotkin Festschrift)
, 2007.

A. Roy,
A. Datta,
A. Derek,
J. C. Mitchell,
J.P. Seifert,
Secrecy Analysis in Protocol Composition Logic,
book chapter in
O. Grumberg, T. Nipkow and C. Pfaller (Editors),
Formal Logical Methods for System Security and Correctness,
Volume 14
NATO Science for Peace and Security Series 
D: Information and Communication Security
,
IOS Press,
March 2008.

D. Garg,
J. Franklin,
D. Kaynar,
A. Datta,
Compositional System Security with InterfaceConfined Adversaries,
to appear in
Proceedings of 26th Annual Conference on Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science
,
May 2010.

Course web page:
Foundations of Security and Privacy at CMU
Proving a Compiler: Mechanized Verification of Program Transformations and Static Analyses — 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 (compilerverification.tar.gz).
References:
Ynot Programming — Greg Morrisett
Nextgeneration 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 sideeffects, 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 higherorder programs with sideeffects, and how to smoothly integrate specifications of those effects into types so that we get a modular treatment of programs with dependency and refinement.
The outcomes for my portion of the summer school are as follows: A student who attends the lectures and does the homework will:
The primary goal is to teach you about the integration of Hoarestyle program logics and type systems, or Hoare Type Theory (HTT). HTT makes it possible to write and reason about imperative, higherorder programs and their computational effects. We can embed HTT into Coq by providing only a very few new primitives. On top of this basic framework, we can define refined versions of HTT that simplify proofs of programs. In particular, we will build a separationbased interface for assembling and reasoning about references and state, and show how this style of interface supports modular reasoning about imperative, abstract data types.
We will also discuss a technique for constructing proofs in Coq that I call "Chlipalastyle" after Adam Chlipala. A Chlipalastyle proof is assembled from a collection of reusable tactics. The tactics are written to be insensitive to as many changes as possible. In particular, the tactics are written to use Ltac's pattern matching to find suitable hypotheses instead of a specific name. Although writing proofs in this style does not come naturally (to me), Adam has convinced me that the resulting proof scripts are easier to maintain than the bruteforce approach that I was used to.
Along the way, we'll study how to build a unificationbased typeinference engine and prove its correctness. We'll first consider a purely functional version of unification, based on a JFP article of Connor McBride, which uses dependent types in a crucial way to ensure termination. Then using the ideas behind HTT, we'll build an imperative version which you can extract to efficient ML code.
References:
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., linkedlists, hashtables, etc.) and algorithms (e.g., unificaton).
Software Foundations in Coq — Benjamin Pierce
Picking up where Andrew Tolmach's lectures leave off (and following the second half of the Software Foundations in Coq text), these lectures will develop more advanced techniques for using a proof assistant to formalize and reason about programming languages. Topics will include formalizations of simple imperative programs, Hoare logic, lambdacalculus, type systems, and the correctness of simple compilers.
Essential Coq from Scratch — Andrew Tolmach
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, based on the early chapters of the textbook Software Foundations in Coq by B. Pierce et al. They will be complemented with plenty of handson exercises.
Lecture topics will include:
Recommended exercises from the first five chapters of Software Foundations: