Fall 2018

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

35% 2 Term Tests

35% Final Exam

SoftwareCourse 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 Hoare Logic Part I Volume 2: Hoare