Explore projects

Utabcert is a Coq formalization of equivalence and containment results obtained by Sagiv and Yannakakis (Equivalence Among Relational Expressions with the Union and Difference Operators).
Updated 
Updated


Updated

Updated


Updated

Updated

Updated

This is a formalisation of Wim Ruitenburg's paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus" (JSL 1984).
Updated 
Software / Reskell
GNU General Public License v3.0 onlyExperimental Haskell implementation of latticevalued resolution.
Updated 
Software / Pihmln
Apache License 2.0A Coq formalization of the HM logic of open bisimulations in picalculus, developed originally by Frederik Haselmeier’s as a part of his MSc thesis with a specific take on the locally nameless approach (called LN_\pi by Frederik)
Updated 
Updated

Updated


HansPeter Deifel / mdpminvalmari
GNU General Public License v3.0 onlyMDP minimization tool from Antti Valmari
Updated 
Updated

BSc project of Alexander Dietsch for simulating LOOP and WHILE programs
Updated 
Software / loopwhileyaccinterpreter
Apache License 2.0Updated 
A Novel Initial Algebra Construction Formalized in Agda
Updated