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.
Course Outline
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
Office Hours
- Tuesday 9:00-11:00 (until December 11)
Lectures
- Morisset Hall Room 219
- Tuesday 14:30-16:00
- Friday 16:00-17:30
Online Textbook
- 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.)- 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)
35% 2 Term Tests
35% Final Exam
Software
Assignments
Exams
- 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
- Covers material from lectures, online textbook, assignments, and quizzes starting from the Tactics chapter up to the end of class on November 16 (plus any material from earlier sections that are required for understanding this material).
- Note: On November 16 we covered the material in Maps.v up to update_example4.
- Closed book
- Final Exam
- Friday, December 14, 14:00-17:00, Learning Crossroads Building (CRX), 100 Louis Pasteur Private, Room C407
- Covers all material from lectures, online textbook, assignments, and quizzes.
- Closed book
Course Outline
-
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-30 |
| Logic in Coq | Volume 1: Logic | October 30-November 6 |
| Inductively Defined Propositions | Volume 1: IndProp | November 6-13 |
| Total and Partial Maps | Volume 1: Maps | November 16-23 |
| Simple Imperative Programs | Volume 1: Imp | November 23-30 |
| Hoare Logic Part I | Volume 2: Hoare | December 4 |
