(3 hours of class per week, 3 credits, categories E,T)
Mathematical underpinnings of reliable software. Topics include basic concepts of logic, computer-assisted theorem proving and the Coq proof assistant, functional programming, operational semantics, Hoare logic, and static type systems.
- Significant programming experience
- Mathematical sophistication
- Undergraduate or graduate functional programming or compiler class
- At least one of:
- Be enrolled in a computer science or math Ph.D. program
- Be enrolled in a computer science or math Master's program with thesis
- Have a computer science 4-year undergraduate degree
- Be an undergraduate in computer science or math with special permission to enroll
Dr. Amy Felty
- Tuesday 9:00-11:00
- Monday, October 15, 12:00-13:00
- Morisset Hall Room 219
- Tuesday 14:30-16:00
- Friday 16:00-17:30
- Software Foundations, Volumes 1 and 2, Benjamin C. Pierce et. al.
Please follow the links below for the versions of these volumes used in this course. (Updated September 5, 2018. Other versions available elsewhere online may be slightly different.)
- Certified Programming with Dependent Types, Adam Chlipala, MIT Press, 2013.
- Interactive Theorem Proving and Program Development--Coq'Art: The Calculus of Inductive Constructions, Springer, 2004.
- Types and Programming Language, Benjamin Pierce, MIT Press, 2002.
30% Assignments (approximately weekly)
35% 2 Term Tests
35% Final Exam
- Term Test 1: Tuesday, October 16
- In class
- Covers material from lectures, online textbook, assignments, and quizzes up to the end of class on October 12.
- You will be provided with Coq code for the definitions of the functions and data structures used on the test.
- Closed book
- Term Test 2: Tuesday, November 20
- In class
- Final Exam
- During final exam period
The course outline will be filled in as the term progresses. This course will follow the online textbooks fairly closely. The list of topics is preliminary.
Topic Textbook Chapters and Notes Date Introduction Volume 1: Preface September 7 Functional Programming in Coq Volume 1: Basics September 7-14 Proof by Induction Volume 1: Induction September 18 Working with Structured Data Volume 1: Lists September 18-October 2 Polymorphism and Higher-Order Functions Volume 1: Poly October 2-9 More Basic Tactics Volume 1: Tactics October 9- Logic in Coq Volume 1: Logic Inductively Defined Propositions Volume 1: IndProp Total and Partial Maps Volume 1: Maps Simple Imperative Programs Volume 1: Imp Hoare Logic Part I Volume 2: Hoare Hoare Logic as a Logic Volume 2: HoareAsLogic