Full text can be accessed here.
This is the repository of my MSc thesis at Chalmers University of Technology. It has been supervised by Thierry Coquand and examined by Nils Anders Danielsson.
The thesis work started on 2019-09-04. The final presentation took place on 2020-05-20 at the ProgLog seminar. Joel Sjögren served as the opponent.
The Agda formalisation in clickable HTML here. The source code is
in code
.