Mechanized Theory

We believe that mechanized formalization and proving play an important role in software development. By implementing a theory in a mechanical prover, one increases its credibility and enables the application of that theory in tools.

In this section you will find theories that our group has implemented in mechanical provers / proof-assistants. Please follow the links on the right for individual projects in this section.