My master's thesis at Utrecht University, including work leading up to it. The result is also preserved on the UU Theses Repository.
src
: Agda codeproject-report
: technical report on a first step, the implementation and correctness proof of dead binding elimination- submitted PDF only, source code is preserved on a separate branch
tyde22
: extended abstract and slides for my talk at TyDe 2022thesis-proposal
: background, preliminary results and schedulethesis
: main thesis documentthesis-defence
: slides for my defence
Developed on:
- Agda 2.6.2.2
- Agda's Standard Library 1.7.1
The code in src/Generic
is based on gallais/generic-syntax,
with some changes:
- reduced to core functionality I needed
- without sized types (these caused complications after recent changes to the Agda compiler)
- with basic support for co-de-Bruijn-based terms, as in Conor McBride's Everybody's Got To Be Somewhere