Verified Programs and Proofs

3 credits

Development of proven-correct programs and computer-checked proofs using functional programming, dependent types and type theory. Topics include constructive logic, the program-proof correspondence, recursion and induction, inductive and indexed data types, statically checked program invariants, and propositional equality proofs. ***Prerequisite: CS 350.***