Written or oral examination. Participation in exercises is required for exam participation.

This course is an introduction to interactive theorem programming and advanced functional programming, mostly using the Coq proof assistant.
This course is for students interested in:
1. The foundational theories of mathematics, most notably type theory and logic
2. Practical interactive theorem proving in a state-of-the-art proof assistant
3. Advanced functional programming languages and their relation to constructive mathematics via the “Curry-Howard Isomorphism”
4. Program verification and “certified programming”
5. Programming Language Semantics

Students will be able to write programs and prove theorems in the Coq proof assistant. Students understand the theoretical underpinnings of interactive theorem
provers and get basic insights into the semantics and formal properties of
programming languages.

Volume 1 and 2 of the “Software Foundations” series available at https://softwarefoundations.cis.upenn.edu/.
A. Chlipala, Certified Programming with Dependent Types, MIT Press / A background in functional programming is helpful. Experience with mathematical proofs is helpful.