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

A generic reasoner for modal and hybrid logics; it can be instantiated to any modal or hybrid logic admitting an axiomatization in terms of socalled rank1 rules or axioms
modal logic hybrid logic coalgebraic ...+ 1 more 

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

BSc project of Michael Banken on simulating counter machines

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:elgotretract.pdf.


Transform bounded selfreference into plain owl files


BSc project of Alexander Dietsch for simulating LOOP and WHILE programs


MDP minimization tool from Antti Valmari

Paul Wild's development of Aarhus ModuRes library



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)