CSCI-799
Mechanized Meta-Theory for Programming Language
Term 20195

General Information

Instructor: Matthew Fluet

E-mail: mtf at cs.rit.edu

Office hours: Mon 3:30pm – 4:30pm; GOL-3555

Wed 2:30pm – 4:30pm; GOL-3555

Fri 10:30am – 11:30am; GOL-3555

Meetings: Mo 10:30am – 11:45am; GOL-3672 (BOR4)

We 10:30am – 11:45am; GOL-3000

Website: http://www.cs.rit.edu/~mtf/teaching/20195/mmt

http://mycourses.rit.edu

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: Fri 17 Jan 2020 10:17:23 PM EST