Fall 2016

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

Course OutlinePrerequisites

- 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

562-5800 ext. 6694

afelty@site.uottawa.ca

Office Hours

- Tuesday 11:30-13:30 (except December 6)
Tuesday, December 6, 14:00-16:00

Lectures

- Monday 11:30-13:00, FTX Room 136
- Thursday 13:00-14:30, SMD Room 402
Last class: Wednesday, December 7, 11:30-13:00, FTX Room 136

Online Textbook

Software Foundations, Benjamin C. Pierce et. al.

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)

35% 2 Term Tests

35% Final Exam

Accounts and SoftwareThis course will use the Coq Proof Assistant. If you want to use it on the machines in the SITE 0110 Computer Lab and don't have an account, you will have to get one. (If you are not an EECS student, you must be registered in the course to get an account. If you are not, see me first.)

Assignments

Exams

- Term Test 1: Thursday, October 13

- In class, SMD Room 402
- Covers material from lectures, online textbook, assignments, and quizzes up to the end of class on October 6.
- 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: Thursday, November 24

- In class, SMD Room 402
- Covers material from lectures, online textbook, assignments, and quizzes starting from the Tactics chapter up to the end of the Maps chapter (plus any material from earlier sections that are required for understanding this material).
- Closed book
Final Exam

- Wednesday, December 21, 14:00-17:00, Wilbrod (WLD), 200 Wilbrod Street, Room 102
- Covers all material from lectures, online textbook, assignments, and quizzes.
- Closed book

Course OutlineThe course outline will be filled in as the term progresses. This course will follow the online textbook fairly closely.

Topic Textbook Chapters and Notes Date Introduction introCSI5140.pdf, Preface September 8 Functional Programming in Coq Basics September 8-15 Proof by Induction Induction September 19 Working with Structured Data Lists September 19-26 Polymorphism and Higher-Order Functions Poly September 26-October 3 More Basic Tactics Tactics October 3-November 3 Logic in Coq Logic November 3-10 Inductively Defined Propositions IndProp November 10-14 Total and Partial Maps Maps November 17 Simple Imperative Programs Imp November 17-December 1 Hoare Logic Part I Hoare December 1-7