CMSC 32001
Topics in Programming Languages
Autumn 2018

General Information

Description

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)

Schedule

Here is a rough schedule for covering the material:

Week 2

• LF: Functional Programming in Coq
• LF: Proof by Induction
• LF: Working with Structured Data

Week 3

• LF: Polymorphism and Higher-Order Functions
• LF: More Basic Tactics
• LF: Logic in Coq

Week 4

** No Meeting **

Week 5

• LF: Inductively Defined Propositions
• LF: Total and Partial Maps
• LF: Simple Imperative Programs
• LF: More Automation

Week 6

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

• PLF: Program Equivalence
• PLF: Hoare Logic, Part I
• PLF: Hoare Logic, Part II

Week 7

• PLF: Small-Step Operational Semantics
• PLF: Types
• PLF: The Simply Typed Lambda-Calculus (STLC)

Week 8

• PLF: The Simply Typed Lambda-Calculus
• PLF: Properties of STLC
• PLF: More on the Simply Typed Lambda-Calculus

Week 9

** No Meeting **

Week 10

• PLF: Typechecking – A Typechecker for STLC
• PLF: References: Typing Mutable References

Resources

Other resources that you might find useful are:

• The Coq Reference Manual

• 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

• An intuitionistic theory of types

• Constructive Mathematics and Computer Programming

Last revised: November 10, 2018