Mécanismes Orientés-Objets pour l'Interopérabilité entre Systèmes de Preuve
Raphaël Cauderlier · HAL - CNAM · 2016
Dedukti is a Logical Framework resulting from the combination ofdependent typing and rewriting. It can be used to encode many logicalsystems using shallow embeddings preserving their notion of reduction.These translations of logical systems in a common format are anecessary first step for exchanging proofs between systems. Thisobjective of interoperability of proof systems is the main motivationof this thesis.To achieve it, we take inspiration from the world of programminglanguages and more specifically from object-oriented languages becausethey feature advanced mechanisms for encapsulation, modularity, anddefault definitions. For this reason we start by a shallowtranslation of an object calculus to Dedukti. The most interestingpoint in this translation is the treatment of subtyping.Unfortunately, it seems very hard to incorporate logic in this objectcalculus. To proceed, object-oriented mechanisms should be restrictedto static ones which seem enough for interoperability. Such acombination of static object-oriented mechanisms and logic is alreadypresent in the FoCaLiZe environment so we propose a shallow embeddingof FoCaLiZe in Dedukti. The main difficulties arise from theintegration of FoCaLiZe automatic theorem prover Zenon and from thetranslation of FoCaLiZe functional implementation language featuringtwo constructs which have no simple counterparts in Dedukti: localpattern matching and recursion.We then demonstrate how this embedding of FoCaLiZe to Dedukti can beused in practice for achieving interoperability of proof systemsthrough FoCaLiZe, Zenon, and Dedukti. In order to avoid strengtheningto much the theory in which the final proof is expressed, we useDedukti as a meta-language for eliminating unnecessary axioms.