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.
Prerequisites
- 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
Professor
-
Dr. Amy Felty
SITE 5-068
afelty@uottawa.ca
Online Textbook
- Software
Foundations, Volumes 1 and 2, Benjamin C. Pierce et. al.
- Volume 1: Logical Foundations
- Volume 2: Programming Language Foundations
Other Resources
- 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.
Evaluation
-
30% Assignments (approximately weekly)
30% 2 Term Tests
10% Project/Presentation
30% Final Exam
Software
- The Coq Proof Assistant
- Coq's main web page is here. Information about how to install Coq on your own computer, as well as further documentation can be found from this page.
- Coq won the 2013 ACM System Software Award.
-
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 |
