Mechanizing Programming Language Metatheory

CIS 700/002
University of Pennsylvania

Fall 2006


Location: Towne 307
Time: MW 1:30-3:00 PM
Instructor: Stephanie Weirich
Prerequisites: CIS 500 (Software foundations) or permission of the instructor

[schedule][references][resources]

Modern proof assistants, such as Coq, Twelf and Isabelle, are mature tools that have been used to create significant bodies of formalized mathematics.  Instead of proving theorems automatically, these tools have achieved great success by working interactively, verifying the small steps of formal reasoning but leaving the main argument of the proof to be supplied. These tools are exactly what the designers of modern programming languages need. They provide a way to formally express the semantics of a modern programming language (at a higher-level than a compiler or interpreter, but more concretely than with English prose) and verify important properties (such as type soundness) about that design.

The goal of this course is to study the foundations for and current practice with modern proof assistants in the context of programming language research. We will learn to use these tools well by studying the type theory that they are based on. The format will be as a discussion course, with grades coming from presentations, class participation and a semester project. Anyone who has taken CIS 500 should be able to take this course.

Date Topic Notes
9/6 Organizational meeting, Overview
Stephanie
9/11 Coquand. Metamathematical Investigations of a Calculus of Constructions. (1989)
(Also, Coquand and Huet.The Calculus of Constructions (1986).)
Stephanie
9/13 The not so simple proof-irrelevance model of CC.
Aaron
9/18* no class
ICFP
9/20* no class
ICFP
9/25 CC continued
Aaron
9/27, 10/2 and 10/4
Paulin-Mohring. Inductive Defininitions in the System Coq Rules and Properties. (1992)
Gimenez and Casteran. A tutorial on recursive types in Coq.
Brian
10/9 and
10/11 and 10/16
Barendregt and Guevers. Proof assistants using dependent type systems. (1999) Geoff
10/18 More about Strong/weak elimination
Dimitrios
10/25 de Bruijn. Checking mathematics with computer assistance.
de Bruijn. A survey of the project AUTOMATH. (1980)
Jeff
10/30 and 11/1
Paulson. The foundation of a generic theorem prover. (1989)
Stephanie
11/6 Paulson. A formulation of the simple theory of types (for Isabelle) (1989)
Stephanie
11/8 Nipkow, Paulson and Wenzel. Isabelle's Logics: HOL
Basin. Higher-order Logic: Foundations
Stephanie
11/13 Harper, Honsell, Plotkin. A Framework for Defining Logics
Brian
11/15 and 11/20 and 11/27 and 11/29
Harper and Licata. Mechanizing Language Definitions. Dimitrios
11/22 No class
Thanksgiving
12/4 Lee, Crary, Harper.  Towards a Mechanized Metatheory of Standard ML. Stephanie
12/6 Wrap-up Stephanie
*indicates dates when Prof. Weirich will be away

Additional references (incomplete list)

Resources for proof development