Explore projects

The Coalgebraic Partition Refiner

The Episciences Remote Control tool for episciences journals like LMCS

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

Template for Bachelor, Master, and Project Theses

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 Novel Initial Algebra Construction Formalized in Agda

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

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

Experimental Haskell implementation of lattice-valued resolution.

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