Explore projects

An abortive attempt by Ulrich R. to formalize de Groote's paper

Coq formalization of guarded iteration a la https://www8.cs.fau.de/_media/research:papers:elgot-retract.pdf.

BSc project of Alexander Dietsch for simulating LOOP and WHILE programs

Paul Wild's development of Aarhus ModuRes library

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).

BSc project of Michael Banken on simulating counter machines

A Coq formalization of "Negative Translations and Normal Modality".

MDP minimization tool from Antti Valmari

A train shunting simulation for the browser.

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...

Transform bounded self-reference into plain owl files

Experimental Haskell implementation of lattice-valued resolution.

A Coq formalization of the HM logic of open bisimulations in pi-calculus, 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)