Universal Algebra, Univalent Foundations and the Untyped λ-Calculus
A.A. van der Leer (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Benedikt Ahrens – Mentor (TU Delft - Programming Languages)
K.F. Wullaert – Mentor (TU Delft - Programming Languages)
Mathijs M. de de Weerdt – Graduation committee member (TU Delft - Algorithmics)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
The λ-calculus is a versatile tool both in mathematical logic and computer science. This thesis studies and expands upon Martin Hyland’s paper ‘Classical lambda calculus in modern dress’. It gives examples for the definitions and provides more detailed proofs, as well as one new proof for Hyland’s fundamental theorem of the λ-calculus. It complements these definitions and proofs with material of previous authors by which Hyland has been inspired. The thesis translates Hyland’s paper from set theory with classical logic to univalent foundations, and showcases where subtleties arise in such a translation. In particular, it discusses the different implementations of the Karoubi envelope in univalent foundations. Lastly, it discusses the accompanying formalization of parts of Hyland’s paper, with in particular a tactic that was developed for applying β-reduction and substitution to λ-terms.