Explore projects

Template for Bachelor, Master, and Project Theses

A train shunting simulation for the browser.

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)

Paul Wild's development of Aarhus ModuRes library

MDP minimization tool from Antti Valmari

Transform bounded self-reference into plain owl files

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

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

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

BSc project of Michael Banken on simulating counter machines

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