Type Theory course ; Master's Degree in Computer Science @ UniPD
-
Updated
Dec 25, 2023 - Agda
Type Theory course ; Master's Degree in Computer Science @ UniPD
📖 Verified Functional Programming in Agda
Extra stuff (mostly math) for Agda.
Metis Prover Reasoning for Propositional Logic in Agda
Homotopy type theory for theorem proving with univalence
Formal proofs in mathematics/computer science/logic formalized in the Agda language. A hobby project I am working on in my free time.
🌐 Theorems that rule this multiverse
A Library for Classical Propositional Logic in Agda
Quite optimized Agda prime numbers generator
Formalization of Regular Languages in Agda: regular expressions, finite-state automata, proof of equivalence, proof of the pumping lemma.
A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses the infrastructure for λ-terms and substitutions provided by the PLFA book
Add a description, image, and links to the theorem-proving topic page so that developers can more easily learn about it.
To associate your repository with the theorem-proving topic, visit your repo's landing page and select "manage topics."