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)
- Dedukti, CoqInE, Holide and Focalide are
here
- Two papers on Dedukti and on encoding logics in Dedukti can be found
here:
- Mathieu Boespflug, Quentin Carbonneaux and Olivier Hermant,
The lambda-Pi-calculus Modulo as a Universal Proof Language, pp. 28-43
- Mathieu Boespflug and Guillaume Burel, CoqInE: Translating the Calculus
of Inductive Constructions into the lambda-Pi-calculus Modulo, pp. 44-50
- Ressources for MMT can be found here.
- Ressources for LATIN can be found here.