Object-Oriented Mechanisms for Interoperability between Proof Systems

Abstract : Dedukti is a Logical Framework resulting from the combination of dependent typing and rewriting. It can be used to encode many logical systems using shallow embeddings preserving their notion of reduction. These translations of logical systems in a common format are a necessary first step for exchanging proofs between systems. This objective of interoperability of proof systems is the main motivation of this thesis. To achieve it, we take inspiration from the world of programming languages and more specifically from object-oriented languages because they feature advanced mechanisms for encapsulation, modularity, and default definitions. For this reason we start by a shallow translation of an object calculus to Dedukti. The most interesting point in this translation is the treatment of subtyping. Unfortunately, it seems very hard to incorporate logic in this object calculus. To proceed, object-oriented mechanisms should be restricted to static ones which seem enough for interoperability. Such a combination of static object-oriented mechanisms and logic is already present in the FoCaLiZe environment so we propose a shallow embedding of FoCaLiZe in Dedukti. The main difficulties arise from the integration of FoCaLiZe automatic theorem prover Zenon and from the translation of FoCaLiZe functional implementation language featuring two constructs which have no simple counterparts in Dedukti: local pattern matching and recursion. We then demonstrate how this embedding of FoCaLiZe to Dedukti can be used in practice for achieving interoperability of proof systems through FoCaLiZe, Zenon, and Dedukti. In order to avoid strengthening to much the theory in which the final proof is expressed, we use Dedukti as a meta-language for eliminating unnecessary axioms.
Document type :
Theses
Complete list of metadatas

https://hal.inria.fr/tel-01415945
Contributor : Raphaël Cauderlier <>
Submitted on : Tuesday, December 13, 2016 - 5:44:27 PM
Last modification on : Wednesday, March 20, 2019 - 4:52:07 PM

File

Licence


Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License

Identifiers

  • HAL Id : tel-01415945, version 1

Citation

Raphaël Cauderlier. Object-Oriented Mechanisms for Interoperability between Proof Systems. Logic in Computer Science [cs.LO]. Conservatoire National Des Arts et Métiers, Paris, 2016. English. ⟨tel-01415945⟩

Share

Metrics

Record views

342

Files downloads

237