Kwarc-Deducteam Workshop, 12 April 2013

Ronan Saillard (Deducteam), Dedukti: a universal proof checker

Dedukti is a type checker for the lambda-Pi-calculus modulo. In this talk I will motivate its use as a universal type checker and detail its theoretical foundations and implementation.

The slides of the presentation are here.

Michael Kohlhase (KWARC), Research in the KWARC Group: Foundations, Interaction, and Semantization

The KWARC research group conducts research in knowledge representation with a view towards applications in knowledge management. We make formal methods modular, scalable, and logic/foundation independent and extend them so that they can be used in settings where formalization is either infeasible or too costly. We concentrate on developing techniques for marking up the structural semantics in technical documents. This level of markup allows for offering interesting knowledge management services without forcing the author to fully formalize the document contents, we are working on methods for semi-automated semantization.

Concretely, we will introduce OMDoc, an open representation format for flexiformal mathematical documents and show applications in active mathematical documents, formula search and semantic help systems.

The slides of the presentation are here.

Florian Rabe (KWARC), The MMT Language and the LATIN logic atlas

MMT is an OMDoc-based representation and interchange language language for formal mathematical knowledge. It permits natural representations of the syntax and semantics of virtually all declarative languages while making MMT-based MKM services easy to implement. Its syntax and semantics are foundationally unconstrained and can be instantiated with specific formal languages and semantic paradigms.

The MMT API implements the MMT language paying special attention to application-independence: It does not provide a runnable application itself but serves as a flexibly reusable kernel library on top of which applications are built. It includes various backends for persistent storage, frontends for machine and user access, logical services such as module system and type reconstruction, as well as knowledge management services such as parsing, querying, and management of change.

The API and all services are generic and can be applied to any formal language represented in MMT. Various plugin interfaces permit injecting syntactic and semantic idiosyncrasies of individual formal languages.

The LATIN atlas is a suite of formalizations of logics and related languages as well as representations between them. It is written in the instantiation of MMT with LF. The atlas includes formalizations of type theories (e.g., lambda cube, Martin-Löf Type Theory and Isabelle), logics (e.g., first-order, higher-order, modal, and description logics) and set theories ( e.g., ZFC, Mizar). All formalizations are systematically modular to maximize reuse and permit building new logic formalizations by recombining existing features.

The documents of the presentation are here.

Ali Assaf (Deducteam), Embedding logics in Dedukti

We show how to express various logics in the lambda-Pi-calculus modulo. Following the Curry-De Bruijn-Howard correspondence, we can view proofs and propositions as terms and types of the lambda-calculus. This allows us to use Dedukti as a universal framework for defining logics and checking proofs in those logics. In this talk, we present a general sound translation of pure type systems in the lambda-Pi-calculus modulo. We show how we adapted this translation to write automatic translators for two proof systems: HOL and Coq.

The slides of the presentation are here.

Mihnea Iancu (KWARC), The OAF Archive of Formalizations and the Mizar Import

The OAF project aims at developing a universal archiving solution for formal mathematical libraries. It will be open to all logical languages and at the same time be aware of their semantics to offer meaningful services. This will provide a permanent archiving solution that not all systems and user communities can afford to maintain separately. And it will establish a standardized and open library format based on OMDoc/MMT that serves as a catalyst for comparison and thus evolution of systems.

The first major import into the OAF was the Mizar library. The Mizar language was formalized as part of LATIN, and an import for the Mizar library was developed based on the MMT API.

OAF will leverage the foundation-independence of the OMDoc/MMT representation language and provide a simple and scalable interface between formal libraries and generic MKM services for them.

Existing services at varying levels of maturity include management of change, search, interactive browsing, forum-like discussions, and metadata management.

The slides of the presentation are here.

Ressources (papers, tools)

Home, Members, Software, Seminars