Explore projects

Paul Wild's development of Aarhus ModuRes library

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

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

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

Template for Bachelor, Master, and Project Theses