(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
- Software Foundations, Volumes 1 and 2, Benjamin C. Pierce et. al.
- 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)
30% 2 Term Tests
30% Final Exam
- The Coq Proof Assistant
The course outline will be filled in as the term progresses. This course will follow the online textbooks fairly closely.
Topic Textbook Chapters Introduction Volume 1: Preface Functional Programming in Coq Volume 1: Basics Proof by Induction Volume 1: Induction Working with Structured Data Volume 1: Lists Polymorphism and Higher-Order Functions Volume 1: Poly More Basic Tactics Volume 1: Tactics 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 More Automation Volume 1: Auto Program Equivalence Volume 2: Equiv Hoare Logic (Part I) Volume 2: Hoare Hoare Logic as a Logic Volume 2: HoareAsLogic Project Presentations