Explore projects

A generic reasoner for modal and hybrid logics; it can be instantiated to any modal or hybrid logic admitting an axiomatization in terms of so-called rank-1 rules or axioms

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

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

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

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

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

A train shunting simulation for the browser.

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

The Coalgebraic Partition Refiner

MDP minimization tool from Antti Valmari

Template for Bachelor, Master, and Project Theses