Browsing Masteruppsatser by Subject "Agda"
Now showing items 1-4 of 4
-
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 ... -
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 ... -
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 ... -
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 ...