Introduction to Dependent Types with Idris: Encoding Program Proofs in Types

© The Author(s), under exclusive license to APress Media, LLC, part of Springer Nature 2023

B. SitnikovskiIntroduction to Dependent Types with Idrishttps://doi.org/10.1007/978-1-4842-9259-4_3

3. Type Theory

Boro Sitnikovski¹  

(1)

Skopje, North Macedonia

 

Some type theories can serve as an alternative foundation of mathematics, as opposed to standard set theory. One such well-known type theory is Martin-Löf’s intuitionistic theory of types, which is an extension of Alonzo Church’s simply-typed λ-calculus. Before you begin working with Idris, you will become familiar with the theories upon which Idris is built as a language.

A shaded circle with the letter ...