• CommProc

    Lecture script to "Kommunikation und Parallele Prozesse", given by Sergey Goncharov in WiSe16.


    • Public Git: git clone git://
    • Member Git: git clone
  • COOL

    COOL - The Coalgebraic Ontology Logic Reasoner

    COOL is 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. Current instantiations include multimodal K (i.e. the description logic ALC), graded modal logic (the Q in ALCQ), and coalition logic (the next-step logic of alternating temporal logic ATL).
    In addition to that COOL also handles many kinds of combinations of these basic logics:

    • Choice A + B: Any world in the model can either have successors according to logic A or to logic B.
    • Fusion A * B: Any world in the model has both successors according to logic A and to B.
    • Sequence A . B: Any wolrd in the model has successors reachable by doing an A-step and then an B-step. (e.g. simple Segala systems which perform an nondeterministic step followed by an probabilistic step).

    COOL currently supports global assumptions, i.e. general TBoxes, nominals, and satisfaction operators; the latter features are similar in expressivity to Boolean ABoxes. COOL implements a global caching algorithm described here (also available here).

    A system description of COOL (COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions, D. Gorin, D. Pattinson, L. Schröder, F. Widmann and T. Wißmann) is forthcoming at IJCAR 2014.


    If you have any questions or patches, feel free to send them via E-Mail.

    Quick links


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

  • countermachine

    BSc project of Michael Banken on simulating counter machines.

    The main link is now

  • cpscoq

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

  • dnegmod

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

    This is not an updated link anymore. The repository has been moved to

  • EnGuard

    Coq formalization of guarded iteration a la


    • Public Git: git clone git://
    • Member Git: git clone
  • lw-simulator

    BSc project of Alexander Dietsch for simulating LOOP and WHILE programs. The repository has been moved to and a successor tool is available as well:

  • MBProg

    Lecture notes on Monad-Based Programming

    held by Dr. Sergey Goncharov in spring semester 2015.

    LaTeX source code

    Obtaining the sources:

      git clone git://

    Preparing and sending patches:...

  • ModuresErl

    Paul Wild's development of Aarhus ModuRes library. The main link now is

  • puzzles

    Material for the Chair presentation at 50 Jahre TechFak

    The assembled material (posters, simulations,...) can be found on
    The train shunting simulation has its own project...

  • Ruitenburg 1984: cycles in IPC

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

    This is not an updated link anymore. The repository has been moved to

  • Shunting

    A train shunting simulation for the browser: Try it online
    For more material, see the Chair Homepage...

  • Utabcert

    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).
    Under the assumption of the results of a recent ESOP paper (A Coq Formalization of the Relational Data Model. V Benzaken, É Contejean, S Dumbrava.) it provides:...

Also available in: Atom