GitHub repository of Agda formalisations

This supercedes all the code below which was written using older versions of Agda and won't work in current versions of Agda.

GitHub repo

Accompanying code from my thesis(deprecated)

Chapter 3

Combinatory Calculus (Basic system).zip

Combinatory Calculus (Finite Products).zip

Combinatory Calculus (Finite Coproducts).zip

Combinatory Calculus (Natural Numbers).zip

Chapter 4

Lambda Calculus (Basic System).zip

Lambda Calculus (Finite Products).zip

Lambda Calculus (Natural Numbers).zip

Chapter 5

Logical Framework - beta (Basic System).zip

Logical Framework - beta-eta (Basic System).zip

Accompanying code from “Type Theory should eat itself”(deprecated)

Partial formalisation of Martin-Löf Type Theory with one universe closed under Π-types in Agda

MLTT.zip

Partial formalisation of Martin-Löf Logical Framework in Agd(deprecated)

LF.zip

Accompanying code from “Big-Step Normalisation”(deprecated)

Formalisation of System T in Agda

System T.zip