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