Projects with this topic
Sort by:
-
Kleine Sammlung an Coq-Aufgaben zum Üben auf Einstiegsniveau.
Updated -
This experimental project aims to build a proof assistant for propositional logic inside another proof assistant: Coq. The main idea is to implement natural deduction rules from the GLoIn-Lecture directly in Coq in order to have a suitable environment to prove stuff in Fitch-Style inside of Coq.
Updated -
Implementation of PCF (inspired by lecture "Monad-Based Programming") in Coq
Updated -
Formalization of numbers (Z,Q, ...), inspired by the lecture "Didaktik der Arithmetik"
Updated -
An attempt at a Coq formalization of Zermelo-Fränkel set theory.
Updated
