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



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 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

AltStyle によって変換されたページ (->オリジナル) /