Search
Now showing items 1-4 of 4
Formalizing domain models of the typed and the untyped lambda calculus in Agda
(2020-12-17)
We present a domain interpretation of the simply typed and the untyped lambda calculus.
The interpretations are constructed using the notion of category with families, with added
structure. Specifically, for the simply ...
A Logical Relation for Dependent Type Theory Formalized in Agda
(2017-02-27)
When writing proofs, it is desirable to show that one’s proof is correct. With
formalising a proof in dependent type theory, it is implied that the proof is correct
as long as the type theory is correct. <br><br> This ...
Formalizing Constructive Quantifier Elimination in Agda
(2018-04-04)
In this thesis a constructive formalization of quantifier elimination is presented,
based on a classical formalization by Tobias Nipkow [16]. The formalization is implemented
and verified in the programming language/proof ...
Agda on Raspberry Pi
(2023-10-25)
This thesis presents an Agda-to-C compiler targeting the Raspberry Pi Pico microcontroller. The compiler implementation includes an unusual choice of run-time algorithm, a Foreign Function Interface generator, and surprisingly ...