This course focuses on interactive theorem proving, i.e. how logical statements can be made precise in a formal machine-checkable language, and how these proofs can be built in the Lean theorem prover. This course will focus on topics in computer science, specifically semantics of programming languages and verification.
Concretely, the course covers:
- Basics of type theory
- Propositions as Types/the Curry-Howard Correspondence
- Proofs with tactics
- Inductive types
- Operational and Denotational Semantics
- Program Logics
- Metaprogramming
- Dozent*in: Andrés Goens