CMSC 32001
Topics in Programming Languages
Autumn 2018

General Information

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.

Elective Credit

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).

Software Foundations

The primary source material will be the first two volumes of Software Foundations:

  1. Logical Foundations (LF)
  2. Programming Language Foundations (PLF)


Here is a rough schedule for covering the material:

Week 2
Week 3
Week 4

** No Meeting **

Week 5
Week 6

For this week, we will start to cover material in Programming Language Foundations.

Week 7
Week 8
Week 9

** No Meeting **

Week 10


Other resources that you might find useful are:

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