Software Foundations
Term 20155

General Information

Instructor: Matthew Fluet
E-mail:  mtf at
Office hours:Mo 2:00pm – 3:00pm; GOL-3555
 Tu 3:00pm – 4:00pm; GOL-3555
 We 11:00am – 12:00pm; GOL-3555
 We 1:00pm – 2:00pm; GOL-3555
 or by appointment
Meetings: TuTh 11:00am – 12:15pm; GOL-3000

Course Description

Much current programming languages research 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), but will also briefly examine other tools and research literature describing the importance of formalized PL research.

Last modified: Wed Feb 3 08:35:31 EST 2016