Mechanized Meta-Theory for Programming Language
Term 20165

General Information

Instructor: Matthew Fluet
E-mail:  mtf at
Office hours:Tu 11:00am – 12:00pm; GOL-3555
 We 11:00am – 12:00pm; GOL-3555
 Th 11:00am – 12:00pm; GOL-3555
 or by appointment
Meetings: TuTh 12:30pm – 1:45pm; GOL-3576 (Breakout Room 3); Week 1
 TuTh 8:00am – 9:15am; GOL-3576 (Breakout Rooom 3)
 and Tu 12:30pm – 1:45pm; GOL-3000
 and Th 12:30pm – 1:45pm; GOL-3672 (Breakout Room 4); Week 2 – 15

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 also examine other tools and research literature describing the importance of formalized PL research during the second half of the semester.

Last modified: Wed Jan 25 16:28:18 EST 2017