Prerequisites: 6.042, 6.005, or equivalent experience with rigorous proofs and programming
Instructor: Professor Adam Chlipala (firstname.lastname@example.org)
Schedule: MW2:30-4, room 34-304
This subject counts as a Computer Systems concentration subject.
An introduction to a spectrum of techniques for rigorous mathematical reasoning about correctness of software, emphasizing commonalities across approaches. The most explicit commonality is formalization of all the different correctness approaches with the Coq proof assistant, a popular software platform for authoring and checking proofs. The beginning of the class will introduce Coq, with the majority of content continuing that introduction in parallel to learning about classic techniques in semantics and program proof. This class is being positioned as a potential future "alternative flavor" of 6.820 and will overlap in coverage of such subjects as operational semantics, basic model checking & abstract interpretation, type systems, and program logics (including separation logic). However, those subjects will take on a different hue viewed through problem sets done fully in Coq, with all grading done automatically by the Coq proof checker. Additional topics will include a variety of approaches to reasoning about concurrency, including through type systems, program logics, and behavioral refinement of interacting modules.