Instructor: | John Reppy |
Crerar 253 | |
Meeting time: | Friday; 1:30-4:50pm |
Location: | Crerar 223 |
The focus of this seminar will be Automated Metatheory (i.e., using Coq or other interactive theorem provers to prove properties of programming languages and/or software systems). The goal of the seminar is the develop the knowledge and skills needed to use Coq on interesting problems.
Ph.D. students who wish to take 32001 for credit as an elective, must inform the instructor by the third week and will be expected to do a project (details to follow).
The primary source material will be the first two volumes of Software Foundations:
Here is a rough schedule for covering the material:
** No Meeting **
For this week, we will start to cover material in Programming Language Foundations.
** No Meeting **
Other resources that you might find useful are:
Certified Programming with Dependent Types by Adam Chlipala (MIT).
Engineering Formal Metatheory by Aydemir et al., POPL 2008.
Arthur Charguéraud's page on the Locally Nameless Representation.
Most examples of interactive proof assistents have their foundations in intuitionistic (or constructive) logic and type theory. Two seminal papers by Per Martin-Löf on these topics are
Last revised: November 10, 2018