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
- Friday, December 10, 16:00-17:00 on Zoom
- Tuesday 10:30-11:30 on Zoom until November 30
- Tuesday 16:00-17:00 in SITE 5-068 until December 7
- Abdorrahim Bahrami (abahr010@uottawa.ca), who is the Corrector for this course, also has office hours by appointment.
Lectures
- Tuesday 14:30-15:50, Social Sciences Building (FSS), Room 1030
- Friday 16:00-17:20, Desmarais Building (DMS), Room 1110
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. 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
-
Your final mark with be determined by one of the following two
formulas, whichever gives you a higher mark:
30% Assignments
30% 2 Term Tests
10% Project/Presentation
30% Final Exam
OR
30% Assignments
35% 2 Term Tests
35% Final Exam
The project is optional. If you choose not to do it, your mark will be determined by the second formula. (See Brightspace for more information.)
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.
Assignments
- Assignments will be given approximately weekly.
- Assignments will be posted on Brightspace.
- Each student is required to do each assignment individually.
- Assignments are due at 20:00 on the date specified. Late submissions will be accepted for up to three days, with a 25% reduction in credit per late day (25% for one day, 50% for two, and 75% for three).
- Assignments must be submitted electronically using your Brightspace account.
Exams
- Term Test 1: Tuesday, October 12
- In class
- Covers material from lectures, online textbook, assignments, and quizzes up to the end of the Poly chapter.
- 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 16
- In class
- Covers material from lectures, online textbook, assignments, and quizzes starting from the Tactics chapter up to the end of the IndProp chapter (plus any material from earlier sections that are required for understanding this material).
- Closed book
- Final Exam
- Saturday, December 11, 19:00-22:00, Lamoureux Hall (LMX), 145 Jean-Jacques-Lussier Private, Room 360
- Covers all material from lectures, online textbook, assignments, and quizzes. The material covered in the Hoare chapter includes up until the end of the "Assignment" subsection in the "Proof Rules" section (up until just before the "Consequence" subsection), and also the "Summary" section at the end.
- 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 to the Course | September 10 | |
| Introduction to the Textbook | Volume 1: Preface | September 14 |
| Functional Programming in Coq | Volume 1: Basics | September 14-21 |
| Proof by Induction | Volume 1: Induction | September 24 |
| Working with Structured Data | Volume 1: Lists | September 24-28 |
| Polymorphism and Higher-Order Functions | Volume 1: Poly | October 1-8 |
| More Basic Tactics | Volume 1: Tactics | October 8-19 |
| Logic in Coq | Volume 1: Logic | October 22-November 5 |
| Inductively Defined Propositions | Volume 1: IndProp | November 5-12 |
| Total and Partial Maps | Volume 1: Maps | November 19 |
| Simple Imperative Programs | Volume 1: Imp | November 23-30 |
| Hoare Logic (Part I) | Volume 2: Hoare | November 30-December 7 |
| Project Presentations | Click here for the schedule | December 2 and 3 |
