LATIN2: Modular Logic Formalizations


Overview

The LATIN2 library of modular logic formalizations supersedes the original LATIN project, which ran from 2009-2012.

LATIN2 is a from-scratch revision of the original LATIN logic formalizations. It is built using and co-evolves with the MMT system. (This is in contrast to LATIN1, which was written in modular Twelf.)

The repository holding the LATIN2 library is [https://gl.mathhub.info/MMT/LATIN2].

Contributors

The main maintainer is Florian Rabe.

It includes contributions from Jonas Betzendahl, Moritz Blöcher, Christian Cerny, Michael Kohlhase, Dennis Müller, Abhik Pal, Navid Roux, Annika Schmidt, Colin Rothgang, Jan Frederik Schaefer, and Sven Wille.

Technical Aspects

For cloning, building, etc. see the documentation in the repository.