Explore projects

Updated

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


Coq formalization of guarded iteration a la https://www8.cs.fau.de/_media/research:papers:elgotretract.pdf.
Updated 
BSc project of Alexander Dietsch for simulating LOOP and WHILE programs
Updated 

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

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

Updated

Updated


Updated

Updated
