Explore projects

Updated


Coq formalization of guarded iteration a la https://www8.cs.fau.de/_media/research:papers:elgotretract.pdf.
Updated 
BSc project of Alexander Dietsch for simulating LOOP and WHILE programs
Updated 

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

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


Experimental Haskell implementation of latticevalued resolution.
Updated 
A 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