CSI 5137
Selected Topics in Software Engineering (Category E)
Fall 2021 · Software Foundations
Topics
- Functional programming in Coq
- Inductive proofs
- Structured data
- Polymorphism and higher-order functions
- Proof tactics
- Logic and inductively defined propositions
- Total and partial maps
- Imperative programs
- Proof automation
- Program equivalence
- Hoare logic
Readings
- Software Foundations, Volume 1: Logical Foundations
- Software Foundations, Volume 2: Programming Language Foundations
- Adam Chlipala, Certified Programming with Dependent Types, MIT Press, 2013.
- Interactive Theorem Proving and Program Development—Coq’Art: The Calculus of Inductive Constructions, Springer, 2004.
- Benjamin Pierce, Types and Programming Languages, MIT Press, 2002.
Sources
- Course catalogue ↗2026–2027
- instructor_course_page ↗Fall 2021
- Crosslisted with Carleton COMP5900 N; follows the online textbooks closely.