4
An introduction to writing computer-verified software and proving mathematical theorems using dependent types. Students will learn to write code using a dependently-typed functional programming language, both to create programs with built-in proofs of correctness and to prove mathematical truths. A main theme of the course is the connection between types and programs on one hand, and propositions and proofs on the other. Other topics include functional programming, algebraic datatypes, and constructive logic. Students who do not meet the COMP 142 prerequisite but have other forms of programming experience are encouraged to reach out to the instructor about enrolling in the course.