Fall 2021

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

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

ProfessorDr. Amy Felty

SITE 5-068

afelty@uottawa.ca

Online Textbook

Software Foundations, Volumes 1 and 2, Benjamin C. Pierce et. al.

Volume 1: Logical FoundationsVolume 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.

Evaluation30% 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.
Course OutlineThe 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