Proofs and Programs 2023 #
This course will introduce Lean Theorem Prover 4, which is an interactive theorem prover as well as a programming language and use it for various aspects of proofs and programs:
- Using programs (interactive theorem provers) to
- verify proofs of results
- help in generating proofs
- Proving correctness of programs
- Writing programs to find and/or verify proofs
- Functional Programming in Lean
To study these things in a meaningful way, we will look at foundations of mathematics and of computation. We will introduce different foundational systems:
- Dependent Type Theory (DTT): foundations used by Lean that include both proofs and computations in a unified way.
- Classical foundations:
- First-order logic: the usual foundations of mathematics.
- lambda-calculus: one of the equivalent formulations of the usual foundations of computation.
Navigation #
To browse the code, expand the PnP2023 tab on the left.