Λέσχη Μαθηματικών

An Introduction to Martin-Löf Type Theory:
A Constructive Approach to Mathematics and Computation

Ανδρέας Αβουκάτος

Περίληψη: Martin-Löf Type Theory (MLTT) provides a constructive foundation for mathematics and computation, integrating logic and type theory in a unified framework. This talk introduces the core principles of MLTT, including dependent types, inductive types, and identity types. We explore how MLTT serves as a foundation for constructive mathematics and influences proof assistants such as Agda. Additionally, we discuss its role in formalising mathematics and its extension in Homotopy Type Theory (HoTT). The talk assumes basic familiarity with mathematical reasoning but does not require prior knowledge of type theory.

Βιβλιογραφία

1. Sandy Maguire, Certainty by Construction, 2023.
2. Aaron Stump, Verified Functional Programming in Agda, 2016.
3. The HoTT game guide
4. Agda readthedocs