© 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 Sitnikovski1  
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 ...

Get Introduction to Dependent Types with Idris: Encoding Program Proofs in Types now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.