Explore projects

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

A train shunting simulation for the browser.

MDP minimization tool from Antti Valmari

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

BSc project of Michael Banken on simulating counter machines

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

Paul Wild's development of Aarhus ModuRes library

BSc project of Alexander Dietsch for simulating LOOP and WHILE programs

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

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