Explore GitLab
Discover projects, groups and snippets. Share your projects with others

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)


Transform bounded selfreference into plain owl files

Experimental Haskell implementation of latticevalued resolution.


Template for Bachelor, Master, and Project Theses



MDP minimization tool from Antti Valmari




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

A train shunting simulation for the browser.

This is a formalisation of Wim Ruitenburg's paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus" (JSL 1984).

Paul Wild's development of Aarhus ModuRes library

BSc project of Alexander Dietsch for simulating LOOP and WHILE programs