Dependent Type Theory with Lean#
Author: Khoa Nguyen
Introduction#
This chapter presents dependent type theory with Lean, demonstrating how types can depend on values and enabling “proofs as programs” through the Curry-Howard correspondence.
Topics#
Dependent type theory foundations
Lean installation and setup
Type inference algorithms
Proofs as programs paradigm
Program verification with dependent types
Resources#
Exercises#
To be added