Mechanized Meta-Theory for Programming Language
Term 20185

General Information

Instructor: Matthew Fluet
E-mail:  mtf at
Office hours:Mon 3:30pm – 4:30pm; GOL-3555
 Wed 2:30pm – 4:30pm; GOL-3555
 Fri 2:30pm – 3:30pm; GOL-3555
Meetings: WeFr 11:00am – 12:15pm; GOL-3672 (BOR4)

Course Description

Much current research in programming languages is being done with the aid of automated proof assistants such as Coq, Isabelle/HOL, Twelf, Agda, NuPRL. This Independent Study will primarily focus on the Coq proof assistant and follow the “Software Foundations” course/text developed by Prof. Benjamin Pierce (UPenn) during the first half of the semester and will examine research literature describing the importance of formalized PL research during the second half of the semester.

Last modified: Tue Jan 22 12:59:37 EST 2019