Formalizing the Zoo of Logical Systems

Michael Kohlhase (Computer Science, FAU Erlangen-Nürnberg, Germany) and Florian Rabe (FAU Erlangen-Nürnberg and LRI Paris)

In this course we present a variety of formal systems from the area of logic and type theory.

We pay attention not (only) to the systems themselves but to their common structural properties.

We show how many diverse systems can be represented systematically and uniformly in a universal meta-logical framework, which allows students to learn both logical systems in general as well as each involved system in particular.

Concrete systems to be studied include but are not limited to propositional logic, first-order logics, modal logics, typed $\lambda$-calculi, functional programming languages, higher-order logics, and axiomatic set theories.

Moreover, students gain hands-on experience by formalizing some of these languages in a logic engineering tool, where complex logics are defined modularly and their implementations prototyped rapidly.