Explore projects
-
Updated
-
-
-
A generic reasoner for modal and hybrid logics; it can be instantiated to any modal or hybrid logic admitting an axiomatization in terms of so-called rank-1 rules or axioms
Updated -
Updated
-
Updated
-
Coq formalization of guarded iteration a la https://www8.cs.fau.de/_media/research:papers:elgot-retract.pdf.
Updated -
Updated
-
Updated
-
-
A Novel Initial Algebra Construction Formalized in Agda
Updated -
-
Updated
-
CORQUE stands for CORecursive eQUations over Effects. This project contains a Coq formalization of complete Elgot monads, their corecursive extensions and background proofs for the paper Unguarded Recursion on Coinductive Resumptions...
Updated -
Updated
-
Updated
-
-
-
Experimental Haskell implementation of lattice-valued resolution.
Updated