Search

Your search keyword '"Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)"' showing total 195 results
Start Over Author "Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)"
195 results on '"Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)"'

1. ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti

Author

Raphaël Cauderlier, Catherine Dubois, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre d'enseignement Cnam Paris (CNAM Paris), Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Deduction modulo, interopérabilité et démonstration automatique ( DEDUCTEAM ), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ), Conservatoire National des Arts et Métiers - Paris ( CNAM Paris ), Conservatoire National des Arts et Métiers [CNAM] ( CNAM ), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise ( ENSIIE ), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification [Cachan] (LSV), and École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Recursion, Programming language, Modulo, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Extension (predicate logic), computer.software_genre, Mathematical proof, 01 natural sciences, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0202 electrical engineering, electronic engineering, information engineering, [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO], Compiler, Rewriting, Pattern matching, computer, Mathematics
Abstract

International audience; The programming environment FoCaLiZe allows the user to specify, implement, and prove programs with the help of the theorem prover Zenon. In the actual version, those proofs are verified by Coq. In this paper we propose to extend the FoCaLiZe compiler by a backend to the Dedukti language in order to benefit from Zenon Modulo, an extension of Zenon for Deduction modulo. By doing so, FoCaLiZe can benefit from a technique for finding and verifying proofs more quickly. The paper focuses mainly on the process that overcomes the lack of local pattern-matching and recursive definitions in Dedukti.

Published
2016
Full Text
View/download PDF

2. Drag Rewriting

Author

Dershowitz, Nachum, Jouannaud, Jean-Pierre, Orejas, Fernando, School of Computer Science (TAU-CS), Tel Aviv University (TAU), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Universitat Politècnica de Catalunya [Barcelona] (UPC)

Subjects
drag morphisms, Graph rewriting, drags, cyclic composition, [INFO]Computer Science [cs], [MATH]Mathematics [math], ACM: F.: Theory of Computation, rewriting
Abstract

We present a new and powerful algebraic framework for graph rewriting, based on drags, a class of graphs enjoying a novel composition operator. Graphs are embellished with roots and sprouts, which can be wired together to form edges. Drags enjoy a rich algebraic structure with sums and products. Drag rewriting naturally extends graph rewriting, dag rewriting, and term rewriting models.

Published
2023

3. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

Author

Sozeau, Matthieu, Forster, Yannick, Lennon-Bertrand, Meven, Nielsen, Jakob, Tabareau, Nicolas, Winterhalter, Théo, Laboratoire des Sciences du Numérique de Nantes (LS2N), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-École Centrale de Nantes (Nantes Univ - ECN), Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST), Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ), Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), University of Cambridge [UK] (CAM), Aarhus University [Aarhus], Département Automatique, Productique et Informatique (IMT Atlantique - DAPI), IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Marie-Curie Grant Agreement No. 101024493.

Subjects
certification, proof assistants, type checker, Coq, [INFO]Computer Science [cs]
Published
2023

4. A theory independent Curry-De Bruijn-Howard correspondence

Author

Dowek, Gilles, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Logic in Computer Science (cs.LO)
Abstract

Instead of developing a customized typed lambda-calculus for each theory, we attempt to design a general parametric calculus that permits to express the proofs of any theory. This way, the problem of expressing proofs in the lambda-calculus is separated from that of choosing a theory.

Published
2023

5. Execution traces and reduction sequences

Author

Dowek, Gilles, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Logic in Computer Science (cs.LO)
Abstract

In this note, we defend that the notion of algorithm as a set of execution traces is somewhat independent of the notion of abstract state machine. It can be reformulated in the more general framework of small step operational semantics.

Published
2023

6. Logipedia: a multi-system encyclopedia of formal proofs

Author

Dowek, Gilles, Thiré, François, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Logic in Computer Science (cs.LO)
Abstract

Libraries of formal proofs are an important part of our mathematical heritage, but their usability and sustainability is poor. Indeed, each library is specific to a proof system, sometimes even to some version of this system. Thus, a library developed in one system cannot, in general, be used in another and when the system is no more maintained, the library may be lost. This impossibility of using a proof developed in one system in another has been noted for long and a remediation has been proposed: as we have empirical evidence that most of the formal proofs developed in one of these systems can also be developed in another, we can develop a standard language, in which these proofs can be translated, and then used in all systems supporting this standard. Logipedia is an attempt to build such a multi-system online encyclopedia of formal proofs expressed in such as standard language. It is based on two main ideas: the use of a logical framework and of reverse mathematics.

Published
2023

7. Explanation: from ethics to logic

Author

Dowek, Gilles, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Logic in Computer Science (cs.LO)
Abstract

When a decision, such as the approval or denial of a bank loan, is delegated to a computer, an explanation of that decision ought to be given with it. This ethical need to explain the decisions leads to the search for a formal definition of the notion of explanation. This question meets older questions in logic regarding the explanatory nature of proof.

Published
2023

8. Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

Author

Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Shenzhen University [Shenzhen]

Subjects
decreasing diagrams, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Mathematics (miscellaneous), orthogonal reductions, Computer Science::Logic in Computer Science, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Church-Rosser property, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], nested critical pairs, Confluence, Computer Science Applications
Abstract

User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom’s decreasing diagrams that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, confluence of a terminating set of left-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. The present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pairs. The rewrite relation used for analyzing confluence may rewrite arbitrarily many non-overlapping redexes in a single step. This relation gives rise to critical pairs that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. Practical examples of use of this technique are analyzed.

Published
2022
Full Text
View/download PDF

9. Traduire l'univers des mathématiques en Dedukti, sans univers

Author

Ledein, Amélie, Butte, Elliot, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Timothy Bourke, and Delphine Demange

Subjects
[INFO]Computer Science [cs]
Abstract

National audience; Ces dernières années, le nombre d'assistants à la preuve, de prouveurs automatiques et de vérificateurs de preuve n'a cessé de croître. L'un d'entre eux, le framework logique Dedukti, a pour objectif de rendre ces outils formels interopérables, c'est-à-dire rendre possible la réutilisation des preuves d'un outil A dans un outil B. Un autre outil formel, Metamath, a la particularité d'être à la 4e place dans la liste des systèmes possédant le plus grand nombre de preuves parmi la liste des 100 théorèmes à prouver de Freek Wiedijk, tout en étant constitué de très peu de fonctionnalités : pas de type dépendant, pas de polymorphisme, ni de notion d'univers. Afin d'agrémenter le nombre de preuves qu'il est possible de traduire dans Dedukti, nous présentons Mathiilde, un traducteur automatique de Metamath vers Dedukti. Comme ce traducteur peut utiliser deux encodages différents de Metamath vers Dedukti, nous discutons les avantages et les inconvénients du point de vue de l'interopérabilité.

Published
2023

10. Recommandations sur les « éditeurs de la zone grise »

Author

Blanqui, Frédéric, Canteaut, Anne, de Jong, Hidde, Imperiale, Sébastien, Mitton, Nathalie, Pallez, Guillaume, Pennec, Xavier, Rival, Xavier, Thirion, Bertrand, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Cryptologie symétrique, cryptologie fondée sur les codes et information quantique (COSMIQ), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Analyse, ingénierie et contrôle des micro-organismes (MICROCOSME), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Grenoble Alpes (UGA), Mathematical and Mechanical Modeling with Data Interaction in Simulations for Medicine (M3DISIM), Laboratoire de mécanique des solides (LMS), École polytechnique (X)-Mines Paris - PSL (École nationale supérieure des mines de Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Mines Paris - PSL (École nationale supérieure des mines de Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Self-organizing Future Ubiquitous Network (FUN), Inria Lille - Nord Europe, Scalable Storage for Clouds and Beyond (KerData), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), E-Patient : Images, données & mOdèles pour la médeciNe numériquE (EPIONE), Inria Sophia Antipolis - Méditerranée (CRISAM), Analyse Statique par Interprétation Abstraite (ANTIQUE), Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Modèles et inférence pour les données de Neuroimagerie (MIND), IFR49 - Neurospin - CEA, Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Inria Saclay - Ile de France, and Inria

Subjects
[INFO]Computer Science [cs], [MATH]Mathematics [math]
Abstract

Recommandations de la Commission d'Évaluation Inria, adoptées le 25 janvier 2023, sur certains éditeurs, notamment MDPI et Frontiers, qui prennent depuis quelques années une place significative dans les domaines de l'informatique et des mathématiques, disciplines où ils étaient absents par le passé.

Published
2023

11. Compositional pre-processing for automated reasoning in dependent type theory

Author

Blot, Valentin, Cousineau, Denis, Crance, Enzo, de Prisque, Louise Dubois, Keller, Chantal, Mahboubi, Assia, Vial, Pierre, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Mitsubishi Electric R&D Centre Europe [France] (MERCE-France), Mitsubishi Electric [France], Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-École Centrale de Nantes (Nantes Univ - ECN), Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST), Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Nantes Université (Nantes Univ), Laboratoire des Sciences du Numérique de Nantes (LS2N), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Calculus of Inductive Constructions, Interactive theorem proving, Arithmetic, Higher order logic, Type theory, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Automated reasoning, Pre-processing, Logic in Computer Science (cs.LO), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Coq
Abstract

International audience; In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of pre-processing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines.

Published
2023
Full Text
View/download PDF

12. Diller-Nahm Bar Recursion

Author

Blot, Valentin, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
Theory of computation → Proof theory, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Bar recursion, Dialectica
Abstract

We present a generalization of Spector’s bar recursion to the Diller-Nahm variant of Gödel’s Dialectica interpretation. This generalized bar recursion collects witnesses of universal formulas in sets of approximation sequences to provide an interpretation to the double-negation shift principle. The interpretation is presented in a fully computational way, implementing sets via lists. We also present a demand-driven version of this extended bar recursion manipulating partial sequences rather than initial segments. We explain why in a Diller-Nahm context there seems to be several versions of this demand-driven bar recursion, but no canonical one., LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 32:1-32:16

Published
2023
Full Text
View/download PDF

13. Une sémantique de K en Dedukti

Author

Ledein, Amélie, Blot, Valentin, Dubois, Catherine, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), and HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)

Subjects
Logical framework, Rewriting, Type theory, [INFO]Computer Science [cs], Programming language, Semantics
Abstract

K is a semantical framework for formally describing the semantics of programming languages thanks to a BNF grammar and rewriting rules on configurations. It is also an environment that offers various tools to help programming with the languages specified in the formalism. For example, it is possible to execute programs thanks to the generated interpreter, or to check some properties of them thanks to the provided automatic theorem prover called the KProver. K is based on Matching Logic, a first-order logic with an application between formulas and a fixed-point, extended with symbols to encode equality, typing and rewriting. This specific Matching Logic theory is called Kore. Dedukti is a logical framework having for main goal the interoperability of proofs between different formal proof tools. Several translators to Dedukti exist or are under development, in order to automatically translate formalizations written, for instance, in Coq or PVS. Dedukti is based on the λΠ-calculus modulo theory, a λ-calculus with dependent types and extended with a primitive notion of computation defined by rewriting rules. The flexibility of this logical framework allows to encode many theories ranging from first-order logic to the Calculus of Constructions. In this article, we present a paper formalization of the translation from K semantics into Kore, and a paper formalization and an automatic translation tool, called KaMeLo, from Kore to Dedukti in order to execute programs in Dedukti.

Published
2022

14. Translating proofs from an impredicative type system to a predicative one

Author

Felicissimo, Thiago, Blanqui, Frédéric, Barnawal, Ashish Kumar, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Indian Institute of Technology Guwahati (IIT Guwahati)

Subjects
FOS: Computer and information sciences, Predicativity, Computer Science - Logic in Computer Science, Type Theory, Universe Polymorphism, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Theory of computation → Type theory, Theory of computation → Logic, Dedukti, Logic in Computer Science (cs.LO), Proof Translation, Unification Modulo Max, Theory of computation → Equational logic and rewriting, Impredicativity, Agda
Abstract

As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics, such as Coq, Matita and the HOL family, to proof assistants based on predicative logics like Agda, whenever impredicativity is not used in an essential way. In this paper we present an algorithm to do such a translation between a core impredicative type system and a core predicative one allowing prenex universe polymorphism like in Agda. It consists in trying to turn a potentially impredicative term into a universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping an impredicative universe to a fixed predicative one is not sufficient in most cases. During the algorithm, we need to solve unification problems modulo the max-successor algebra on universe levels. But, in this algebra, there are solvable problems having no most general solution. We however provide an incomplete algorithm whose solutions, when it succeeds, are most general ones. The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool Predicativize and then used to translate semi-automatically many non-trivial developments from Matita’s arithmetic library to Agda, including Bertrand’s Postulate and Fermat’s Little Theorem, which were not available in Agda yet., LIPIcs, Vol. 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pages 19:1-19:19

Published
2022

15. A direct computational interpretation of second-order arithmetic via update recursion

Author

Blot, Valentin, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; Second-order arithmetic has two kinds of computational interpretations: via Spector's bar recursion of via Girard's polymorphic lambda-calculus. Bar recursion interprets the negative translation of the axiom of choice which, combined with an interpretation of the negative translation of the excluded middle, gives a computational interpretation of the negative translation of the axiom scheme of comprehension. It is then possible to instantiate universally quantified sets with arbitrary formulas (second-order elimination). On the other hand, polymorphic lambda-calculus interprets directly second-order elimination by means of polymorphic types. The present work aims at bridging the gap between these two interpretations by interpreting directly second-order elimination through update recursion, which is a variant of bar recursion.

Published
2022
Full Text
View/download PDF

16. An Implementation of Set Theory with Pointed Graphs in Dedukti

Author

Blot, Valentin, Dowek, Gilles, Traversié, Thomas, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; DEDUKTI is a type-checker for the λ Π-calculus modulo theory, a logical framework that allows the extension of conversion with user-defined rewrite rules. In this paper, we present the implementation of a version of Dowek-Miquel's intuitionistic set theory in DEDUKTI. To do so, we adapt this theory-based on the concept of pointed graphs-from Deduction modulo theory to λ Π-calculus modulo theory, and we formally write the proofs in DEDUKTI. In particular, this implementation requires the definition of a deep embedding of a certain class of formulas, as well as its interpretation in the theory.

Published
2022

17. Bécassine à la chasse au Coq (démonstration)

Author

Blot, Valentin, Dubois de Prisque, Louise, Keller, Chantal, Vial, Pierre, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Chantal Keller, and Timothy Bourke

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

National audience; Nous présentons une nouvelle tactique Coq (snipe) permettant de prouver automatiquement des butsCoq en les envoyant à des prouveurs automatiques externes du premier ordre via des plugins. Pour ce faire, la tactique snipe réduit le but à un énoncé du premier ordre et enrichit le contexte local avec des énoncés explicitant pour le prouveur la sémantique du but. Nous combinons des transformations modulaires et indépendantes permettant chacune de réduire un aspect spécifique du langage de Coq au langage (plussimple) d’un prouveur automatique. A l’heure actuelle, snipe utilise des transformations simples mais cruciales qui explicitent des définitions et des types algébriques. Ceci permet de prouver automatiquementdes buts mêlant raisonnement au premier ordre, types de données et polymorphisme. Ce prototype de tactique automatique est un premier pas vers l’implantation et la combinaison de transformations plus complexes, qui rendront Coq plus facile d’accès.

Published
2022

18. Vers une traduction de K en Dedukti

Author

Ledein, Amélie, Blot, Valentin, Dubois, Catherine, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Chantal Keller, and Timothy Bourke

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ComputingMilieux_MISCELLANEOUS
Abstract

National audience

Published
2022

19. Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting

Author

Michael Färber, University of Innsbruck, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Leopold Franzens Universität Innsbruck - University of Innsbruck

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, reduction, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Dedukti, type checking, 0202 electrical engineering, electronic engineering, information engineering, concurrency, Interactive proof systems, CCS Concepts: • Theory of computation → Logic and verification, Equational logic and rewriting, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Automated reasoning, Higher order logic concurrency, Logic in Computer Science (cs.LO), rewriting, sharing, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Rust, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, verification, performance
Abstract

Several proof assistants, such as Isabelle or Coq, can concurrently check multiple proofs. In contrast, the vast majority of today's small proof checkers either does not support concurrency at all or only limited forms thereof, restricting the efficiency of proof checking on multi-core processors. This work shows the design of a small, memory- and thread-safe kernel that efficiently checks proofs both concurrently and non-concurrently. This design is implemented in a new proof checker called Kontroli for the lambda-Pi calculus modulo rewriting, which is an established framework to uniformly express a multitude of logical systems. Kontroli is faster than the reference proof checker for this calculus, Dedukti, on all of five evaluated datasets obtained from proof assistants and interactive theorem provers. Furthermore, Kontroli reduces the time of the most time-consuming part of proof checking using eight threads by up to 6.6x., 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '22), Jan 2022, Philadelphia, PA, United States

Published
2022
Full Text
View/download PDF

20. Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity

Author

Blanqui, Frédéric, Centre National de la Recherche Scientifique (CNRS), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], type universes, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], rewriting theory, Theory of computation → Type theory, Theory of computation → Logic, rewriting, associativity and commutativity, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, logical framework, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, type theory, Theory of computation → Equational logic and rewriting
Abstract

The encoding of proof systems and type theories in logical frameworks is key to allow the translation of proofs from one system to the other. The λΠ-calculus modulo rewriting is a powerful logical framework in which various systems have already been encoded, including type systems with an infinite hierarchy of type universes equipped with a unary successor operator and a binary max operator: Matita, Coq, Agda and Lean. However, to decide the word problem in this max-successor algebra, all the encodings proposed so far use rewriting with matching modulo associativity and commutativity (AC), which is of high complexity and difficult to integrate in usual algorithms for b-reduction and type-checking. In this paper, we show that we do not need matching modulo AC by enforcing terms to be in some special canonical form wrt associativity and commutativity, and by using rewriting rules taking advantage of this canonical form. This work has been implemented in the proof assistant Lambdapi., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 24:1-24:14

Published
2022
Full Text
View/download PDF

21. From the Universality of Mathematical Truth to the Interoperability of Proof Systems

Author

Dowek, Gilles, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
[MATH.MATH-LO]Mathematics [math]/Logic [math.LO], [INFO]Computer Science [cs]
Abstract

International audience; The development of computerized proof systems, such as Coq, Matita, Agda, Lean, HOL 4, HOL Light, Isabelle/HOL, Mizar, etc. is a major step forward in the never ending quest of mathematical rigor. But it jeopardizes the universality of mathematical truth [5]: we used to have proofs of Fermat's little theorem, we now have Coq proofs of Fermat's little theorem, Isabelle/HOL proofs of Fermat's little theorem, PVS proofs of Fermat's little theorem, etc. Each proof system: Coq, Isabelle/HOL, PVS, etc. defining its own language for mathematical statements and its own truth conditions for these statements. This crisis can be compared to previous ones, when mathematicians have disagreed on the truth of some mathematical statements: the discovery of the incommensurability of the diagonal and side of a square, the introduction of infinite series, the non-Euclidean geometries, the discovery of the independence of the axiom of choice, and the emergence of constructivity. All these past crises have been resolved.

Published
2022
Full Text
View/download PDF

22. Geometry of Interaction for ZX-Diagrams

Author

Chardonnet, Kostia, Valiron, Benoît, Vilmart, Renaud, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), CentraleSupélec, ANR-17-CE25-0009,SoftQPRO,Solutions logicielles pour l'optimisation des programmes et ressources quantiques(2017), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Quantum Computation Structures (QuaCS), and Gouat, Isabelle

Subjects
Quantum Computation, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Quantum Physics, Theory of computation → Linear logic, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], FOS: Physical sciences, Linear Logic, Geometry of Interaction, Logic in Computer Science (cs.LO), [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Theory of computation → Quantum computation theory, ZX-Calculus, Theory of computation → Equational logic and rewriting, Quantum Physics (quant-ph)
Abstract

ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from Geometry of Interaction, in this paper we propose a token-machine-based asynchronous model of both pure ZX-Calculus and its extension to mixed processes. We also show how to connect this new semantics to the usual standard interpretation of ZX-diagrams. This model allows us to have a new look at what ZX-diagrams compute, and give a more local, operational view of the semantics of ZX-diagrams., LIPIcs, Vol. 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), pages 30:1-30:16

Published
2022
Full Text
View/download PDF

23. Adequate and Computational Encodings in the Logical Framework Dedukti

Author

Felicissimo, Thiago, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Logical Frameworks, Rewriting, Type Theory, Pure Type Systems, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Theory of computation → Equational logic and rewriting, Data_CODINGANDINFORMATIONTHEORY, Theory of computation Ñ Equational logic and rewriting phrases Type Theory, Theory of computation → Type theory, Dedukti, Logic in Computer Science (cs.LO)
Abstract

Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (LF), allows for the representation of computation alongside deduction. However, unlike LF encodings, Dedukti encodings proposed until now do not feature an adequacy theorem - i.e., a bijection between terms in the encoded system and in its encoding. Moreover, many of them also do not have a conservativity result, which compromises the ability of Dedukti to check proofs written in such encodings. We propose a different approach for Dedukti encodings which do not only allow for simpler conservativity proofs, but which also restore the adequacy of encodings. More precisely, we propose in this work adequate (and thus conservative) encodings for Functional Pure Type Systems. However, in contrast with LF encodings, ours is computational - that is, represents computation directly as computation. Therefore, our work is the first to present and prove correct an approach allowing for encodings that are both adequate and computational in Dedukti., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 25:1-25:18

Published
2022
Full Text
View/download PDF

24. Classical Simulation of Quantum Circuits with Partial and Graphical Stabiliser Decompositions

Author

Kissinger, Aleks, van de Wetering, John, Vilmart, Renaud, University of Oxford, Quantum Computation Structures (QuaCS), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Radboud University [Nijmegen], and Gall, F. Le

Subjects
Quantum Physics, [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Stabiliser Rank, Theory of computation → Quantum computation theory, Quantum Simulation, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], FOS: Physical sciences, ZX-calculus, Digital Security, Quantum Physics (quant-ph)
Abstract

Recent developments in classical simulation of quantum circuits make use of clever decompositions of chunks of magic states into sums of efficiently simulable stabiliser states. We show here how, by considering certain non-stabiliser entangled states which have more favourable decompositions, we can speed up these simulations. This is made possible by using the ZX-calculus, which allows us to easily find instances of these entangled states in the simplified diagram representing the quantum circuit to be simulated. We additionally find a new technique of partial stabiliser decompositions that allow us to trade magic states for stabiliser terms. With this technique we require only 2^{α t} stabiliser terms, where α≈ 0.396, to simulate a circuit with T-count t. This matches the α found by Qassim et al. [Qassim et al., 2021], but whereas they only get this scaling in the asymptotic limit, ours applies for a circuit of any size. Our method builds upon a recently proposed scheme for simulation combining stabiliser decompositions and optimisation strategies implemented in the software QuiZX [Kissinger and van de Wetering, 2022]. With our techniques we manage to reliably simulate 50-qubit 1400 T-count hidden shift circuits in a couple of minutes on a consumer laptop., LIPIcs, Vol. 232, 17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022), pages 5:1-5:13

Published
2022
Full Text
View/download PDF

25. Unification of drags and confluence of drag rewriting

Author

Jouannaud, Jean-Pierre, Orejas, Fernando, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Universitat Politècnica de Catalunya [Barcelona] (UPC), Jouannaud, Jean-Pierre, Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire de Méthodes Formelles, Université de Paris-Saclay, Université de Paris Saclay, Universitat Politècnica de Catalunya. Departament de Ciències de la Computació, and Universitat Politècnica de Catalunya. ALBCOM - Algorísmia, Bioinformàtica, Complexitat i Mètodes Formals

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], unification, InformationSystems_INFORMATIONINTERFACESANDPRESENTATION(e.g.,HCI), Logic, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], GeneralLiterature_MISCELLANEOUS, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Theoretical Computer Science, Physics::Fluid Dynamics, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Drags, Algorismes computacionals, ComputingMethodologies_COMPUTERGRAPHICS, graphs, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Confluence, ACM: D.: Software, Computer algorithms, ACM: F.: Theory of Computation, Informàtica::Informàtica teòrica::Algorísmica i teoria de la complexitat [Àrees temàtiques de la UPC], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, Unification, [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, confluence, Computer Science::Programming Languages, Astrophysics::Earth and Planetary Astrophysics, Graphs, Software
Abstract

Drags are a recent, natural generalization of terms which admit arbitrary cycles. A key aspect of drags is that they can be equipped with a composition operator so that rewriting amounts to replace a drag by another in a composition. In this paper, we develop a unification algorithm for drags that allows to check the local confluence property of a set of drag rewrite rules. This work is partially supported by MCIN/AEI /10.13039/501100011033 under grant PID2020-112581GB-C21.

Published
2023
Full Text
View/download PDF

26. M1 Internship ReportTranslating proofs between Isabelle and Dedukti

Author

Leray, Yann, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Deducteam - Inria Paris-Saclay / ENS Paris-Saclay

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Published
2021

27. Integrating Automated Theorem Provers in Proof Assistants

Author

El Haddad, Yacine, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Université Paris-Saclay, Frédéric Blanqui, and Guillaume Burel

Subjects
Assistants à la preuve, Type theory, Reconstruction de preuves, [INFO.INFO-AU]Computer Science [cs]/Automatic Control Engineering, Proof reconstruction, Skolemization, Démonstration automatique, Théorie des types, Proof assistant, Automated deduction
Abstract

Lambdapi is a proof assistant that allows users to construct a proof of a given theorem in a universal language based on the lambda-pi-calculus. The goal of this thesis is to add more automation to Lambdapi to gain more time and effort for the users. This thesis presents three contributions associated with the integration of automated provers in proof assistants. The first contribution consists of the implementation of a tactic that calls automated provers from Lambdapi by using an external platform called Why3. Usually, automated provers do not generate a complete certificate of a given formula, thus, the second contribution presented in this thesis is the reconstruction in Lambdapi of proofs generated by first-order automated provers implemented in a tool called Ekstrakto. Finally, automated provers often perform some transformations on the formula that they are trying to solve. Among these transformations, we can find Skolemization steps. The last contribution is devoted to the certification of Skolemization steps performed by the automated provers in order to have a complete reconstruction. This has been implemented in a tool called Skonverto.; Lambdapi est un assistant de preuve qui permet à l’utilisateur la construction d’une preuve d’un théorème donné dans un langage universel basé sur le lambda-pi-calcul. Le but de cette thèse est de rajouter de l’automatisation à Lambdapi pour faire gagner du temps à l’utilisateur. Cette thèse présente trois contributions liées à l’intégration des démonstrateurs automatiques dans les assistants de preuve. La première contribution consiste en l’implémentation d’une tactique qui fait appel au démonstrateurs automatiques depuis Lambdapi à travers une plateforme tiers appelé Why3. Généralement, les démonstrateurs automatiques ne génèrent pas un certificat de preuve complet, d’où la deuxième contribution présentée dans cette thèse: la reconstruction de preuves générées par les démonstrateurs automatiques du premier ordre dans Lambdapi implémenté dans un outil appelé Ekstrakto. Enfin, ces démonstrateurs peuvent parfois effectuer des modifications sur la formule qu'ils sont en train de prouver. Le dernier résultat de la thèse est consacré à la certification des étapes de Skolemisation faites par les démonstrateurs automatiques. Un algorithme est présenté, montré correct et impleménté dans l'outil Skonverto.

Published
2021

28. Representing Agda and coinduction in the λΠ-calculus modulo rewriting

Author

Felicissimo, Thiago, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), LSV, ENS Paris Saclay, Université Paris-Saclay, Frederic Blanqui, and Gilles Dowek

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; Coinduction is a principle, or a proof technique, dual to induction and which allows to handle possibly infinite objects in a natural way, such as infinite lists, infinite trees, formal languages, non well-founded sets, etc. Because of its usefulness, it is increasingly being added to proof assistants, such as Coq, Isabelle, PVS and Agda. In order to be able to translate proofs by coinduction coming from multiple proof assistants it is thus important to first understand how to encode coinduction in Dedukti, a problem that had never been addressed before. During this internship, we studied the representation of Agda and coinduction in Dedukti. Among the techniques of implementing coinduction in proof assistants, Agda features two presentations: musical coinduction and copattern coinduction. Based on their internal syntax representation in Agda, we proposed an encoding of both presentations in Dedukti. We resumed the development of the Agda2Dedukti translator and extended it with the proposed encoding, allowing it to translate automatically proofs by coinduction into Dedukti.

Published
2021

29. Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories

Author

Jean-Pierre Jouannaud, Gaspard Férey, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
higher-order rewrite rules, term layers, Computer science, non-linear patterns, 0102 computer and information sciences, Lambda, Mathematical proof, 01 natural sciences, sub-rewriting, Dependent type theory, Computer Science::Logic in Computer Science, Order (group theory), 0101 mathematics, computer.programming_language, Lambda calculus, decreasing diagrams, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 16. Peace & justice, Algebra, 010201 computation theory & mathematics, higher-order critical pairs, Confluence, confluence, Church-Roser property, Computer Science::Programming Languages, computer
Abstract

International audience; We develop techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of critical pairs for higher-order rewrite rules extending betareduction on pure lambda-terms. We show that confluence is preserved for a large subset of terms that contains all pure lambda terms. Our results are applied to famous Klop's examples of non-confluent behaviours in lambda-calculi with convergent rewrite rules, on the one hand, and to fragments of an encoding in a dependent type theory augmented with rewrite rules of the Calculus of Constructions with polymorphic universes.

Published
2021
Full Text
View/download PDF

30. Some Axioms for Mathematics

Author

Blanqui, Frédéric, Dowek, Gilles, Grienenberger, Émilie, Hondet, Gabriel, Thiré, François, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Nomadic Labs

Subjects
interoperabilty, dependent types, Type theory, Logic, axiomatic theory, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Theory of computation → Type theory, Theory of computation → Logic, rewriting, Logical framework, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computer Science::Logic in Computer Science, Theory of computation → Equational logic and rewriting, Computer Science::Databases
Abstract

The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 20:1-20:19

Published
2021
Full Text
View/download PDF

31. Drags: A compositional algebraic framework for graph rewriting

Author

Jean-Pierre Jouannaud, Nachum Dershowitz, Tel Aviv University (TAU), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Université Paris-Saclay, Deducteam, and Tel Aviv University [Tel Aviv]

Subjects
Vertex (graph theory), General Computer Science, Computer science, Generalization, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Term algebra, ACM: G.: Mathematics of Computing, Theoretical Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Drags, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Algebraic number, Graph rewriting, symmetric monoidal category, Symmetric monoidal category, Function (mathematics), Graph, rewriting, Vertex (geometry), Algebra, 010201 computation theory & mathematics, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, Rewriting, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Graphs, MathematicsofComputing_DISCRETEMATHEMATICS
Abstract

International audience; We are interested in a natural generalization of term-rewriting techniques to what we call drags, viz. finite, directed, ordered, rooted multigraphs, each vertex of which is labeled by a function symbol. To this end, we develop a rich algebra of drags that generalizes the familiar term algebra and its associated rewriting capabilities. Viewing graphs as terms provides an initial building block for rewriting with such graphs, one that should impact the many areas where computations take place on graphs.

Published
2019
Full Text
View/download PDF

32. Higher-Order Confluence and Universe Embedding in the Logical Framework

Author

Ferey, Gaspard, Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris-Saclay, Gilles Dowek, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
Méthodes formelles, Formal methods, Traduction de logiques, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Confluence, Rewriting techniques, Réécriture, Logic system translation, Termination, Terminaison
Abstract

In the context of the multiplicity of formal systems, it has become a growing need to express formal proofs into a common logical framework.This thesis focuses on the use of higher-order term rewriting to embed complex formal systems in the simple and well-studied lambda-Pi calculus modulo.This system, commonly used as a logical framework, features dependent types and is extended with higher-order term rewriting.We study, in a first part, criterias for the confluence properties of higher-order rewrite systems considered together with the usual beta reduction.In the case of left-linear systems, confluence can be reduced to the study of critical pairs which must be provided a decreasing diagram with relation to some rule labeling.We show that in the presence of non-linear rules, it is still possible to achieve confluence if the set of considered terms is layered.We then focus, in a second part, on the encoding of higher-order logics based on complex universe structures. The embeding of cumulativity, a limited form of subtyping, is handled with new rewriting techniques relying on private symbols and allowing some form of proof irrelevance.We then describe how algebraic universe expressions containing level variables can be represented, even in presence of universe constraints.Eventually we introduce an embeding of universe polymorphism as defined in the core logic of the Coq system and prove the correctness of the defined translation mechanism.These results, along with other more practical techniques, allowed the implementation of a translator to Dedukti which was used to translate several sizeable Coq developments.; La multiplicité des systèmes formels a mis en évidence la nécessité d'un socle logique commun dans lequel les formalismes logiques pourraient être exprimés.L'enjeu principal de ce manuscrit est la définition de techniques d'encodages reposant sur la réécriture de termes et capables de réprésenter les fonctionnalités avancées des systèmes de types modernes.Nos encodages s'appuieront sur le lambda-Pi calcul modulo, un système de types dépendants, communément utilisé comme cadre logique, étendu ici par de laréécriture d'ordre supérieur. On s'intéresse, dans une première partie, aux critères de confluence de systèmes de réécriture avec la bêta réduction.La confluence d'un système linéaire à gauche se déduit de l'étude de ses paires critiques pour lesquelles il faut exhiber un diagramme décroissant vis-à-vis d'un certain étiquetage des règles.Le cas non-linéaire nécessite, lui, une compartimentalisation des termes considérés.On considère, dans un second temps, l'encodage de systèmes de types complexes.Sont étudiés successivement, la cumulativité qui nécessite de considérer des symboles privés pour encoder une forme de ``proof irrelevance'', les expressions algébriques d'univers sous contraintes d'univers et enfin le polymorphisme d'univers dont on prouve la correction d'une fonction de traduction depuis un sous-ensemble de Coq.L'implantation de ces résultats a permis de traduire en Dedukti plusieurs développements Coq de taille significative.

Published
2021

33. Confluence in UnTyped Higher-Order Theories by means of Critical Pairs

Author

Férey, Gaspard, Jouannaud, Jean-Pierre, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Church-Rosser property, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Confluence, Type systems, [INFO]Computer Science [cs], Ancestor peaks, Critical peaks, Decreasing diagrams, Lambda calculus
Abstract

User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. We develop here techniques that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. The present paper concentrates on the case where rewrite rules are left-linear and critical pairs can be joined without using beta-rewrite steps. The other two cases will be addressed in forthcoming papers.

Published
2021

34. Confluence in non-left-linear higher-order theories

Author

Férey, Gaspard, Jouannaud, Jean-Pierre, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Université Paris-Saclay – ENS Paris-Saclay – Sorbonne Université

Subjects
Computer Science::Logic in Computer Science, Computer Science::Programming Languages, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

We develop techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of critical pairs for higher-order rewrite rules extending betareduction on pure lambda-terms. We show that confluence is preserved for a large subset of terms that contains all pure lambda terms. Our results are applied to famous Klop's examples of non-confluent behaviours in lambda-calculi with convergent rewrite rules, on the one hand, and to fragments of an encoding in a dependent type theory augmented with rewrite rules of the Calculus of Constructions with polymorphic universes. on the other hand.

Published
2021

35. Small, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting

Author

Färber, Michael, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
sharing, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, type checking, Rust, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], reduction, concurrency, verification, Dedukti, performance, rewriting
Abstract

Several proof assistants, such as Isabelle or Coq, can concurrently check multiple proofs. In contrast, the vast majority of today's small proof checkers either does not support concurrency at all or only limited forms thereof, restricting the efficiency of proof checking on multi-core processors. This work presents a small proof checker with support for concurrent proof checking, achieving state-of-the-art performance in both concurrent and nonconcurrent settings. The proof checker implements the lambda-Pi calculus modulo rewriting, which is an established framework to uniformly express a multitude of logical systems. The proof checker is faster than the reference proof checker for this calculus, Dedukti, on all of five evaluated datasets obtained from proof assistants and interactive theorem provers.

Published
2021

36. Confluence of Non-Terminating Left-Linear Higher-Order Rewrite Theories

Author

Dowek, Gilles, Férey, Gaspard, Jouannaud, Jean-PIerre, Liu, Jiaxiang, Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Shenzhen Institute of Advanced Technology [Shenzhen] (SIAT), Chinese Academy of Sciences [Beijing] (CAS), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, decreasing diagrams, orthogonal reductions, Computer Science::Logic in Computer Science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Confluence, nested critical pairs
Abstract

User-de ned higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. is raises the question of proving that they preserve the properties of β-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom's decreasing diagrams that reduce con uence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, con uence of a terminating set of le-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. e present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pars. e rewrite relation used for analyzing con uence, called orthogonal, gives rise to critical pairs, called nested, that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. is second paper terminates our investigation of con uence in the case of le-linear rules.

Published
2021

37. Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory

Author

Valentin Maestracci, Bruno Barras, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), and Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 02 engineering and technology, Type (model theory), 16. Peace & justice, Logic in Computer Science (cs.LO), Algebra, Logical framework, Type theory, 0202 electrical engineering, electronic engineering, information engineering, Encoding (semiotics), 020201 artificial intelligence & image processing, Layer (object-oriented design), De Morgan algebra, Mathematics
Abstract

In this paper, we make a substantial step towards an encoding of Cubical Type Theory (CTT) in the Dedukti logical framework. Type-checking CTT expressions features a decision procedure in a de Morgan algebra that so far could not be expressed by the rewrite rules of Dedukti. As an alternative, 2 Layer Type Theories are variants of Martin-L\"of Type Theory where all or part of the definitional equality can be represented in terms of a so-called external equality. We propose to split the encoding by giving an encoding of 2 Layer Type Theories (2LTT) in Dedukti, and a partial encoding of CTT in 2LTT., Comment: In Proceedings LFMTP 2020, arXiv:2101.02835

Published
2021

38. General Automation in Coq through Modular Transformations

Author

Valentin Blot, Chantal Keller, Louise Dubois de Prisque, Pierre Vial, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer science, business.industry, Programming language, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Context (language use), Modular design, computer.software_genre, Automation, Logic in Computer Science (cs.LO), Set (abstract data type), Type theory, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Simple (abstract algebra), Proof of concept, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Algebraic data type, business, computer
Abstract

Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further away from first-order logic, the logic of most automatic theorem provers. In this article, we develop a methodology to transform a subset of Coq goals into first-order statements that can be automatically discharged by automatic provers. The general idea is to write modular, pairwise independent transformations and combine them. Each of these eliminates a specific aspect of Coq logic towards first-order logic. As a proof of concept, we apply this methodology to a set of simple but crucial transformations which extend the local context with proven first-order assertions that make Coq definitions and algebraic types explicit. They allow users of Coq to solve non-trivial goals automatically. This methodology paves the way towards the definition and combination of more complex transformations, making Coq more accessible., Comment: In Proceedings PxTP 2021, arXiv:2107.01544

Published
2021
Full Text
View/download PDF

39. Interacting Safely with an Unsafe Environment

Author

Gilles Dowek, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Programming language, Computer science, media_common.quotation_subject, Computation, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Type (model theory), computer.software_genre, Logic in Computer Science (cs.LO), Presentation, Logical framework, Unsafe environment, computer, media_common
Abstract

We give a presentation of Pure type systems where contexts need not be well-formed and show that this presentation is equivalent to the usual one. The main motivation for this presentation is that, when we extend Pure type systems with computation rules, like in the logical framework Dedukti, we want to declare the constants before the computation rules that are needed to check the well-typedness of their type., Comment: In Proceedings LFMTP 2021, arXiv:2107.07376

Published
2021
Full Text
View/download PDF

40. Quantum Multiple-Valued Decision Diagrams in Graphical Calculi

Author

Vilmart, Renaud, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Quantum Physics, Computer Science - Logic in Computer Science, Quantum Decision Diagrams, FOS: Physical sciences, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Categorical Quantum Mechanics, Decision Diagrams, ZH-Calculus, Logic in Computer Science (cs.LO), [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Theory of computation → Quantum information theory, ComputerSystemsOrganization_MISCELLANEOUS, Normal Form, Theory of computation → Equational logic and rewriting, Quantum Computing, Quantum Physics (quant-ph)
Abstract

Graphical calculi such as the ZH-calculus are powerful tools in the study and analysis of quantum processes, with links to other models of quantum computation such as quantum circuits, measurement-based computing, etc. A somewhat compact but systematic way to describe a quantum process is through the use of quantum multiple-valued decision diagrams (QMDDs), which have already been used for the synthesis of quantum circuits as well as for verification. We show in this paper how to turn a QMDD into an equivalent ZH-diagram, and vice-versa, and show how reducing a QMDD translates in the ZH-Calculus, hence allowing tools from one formalism to be used into the other., LIPIcs, Vol. 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), pages 89:1-89:15

Published
2021
Full Text
View/download PDF

41. Terminaison en présence de types dépendants et encodage par réécriture d’une théorie des types extensionelle avec polymorphisme d’univers

Author

Genestier, Guillaume, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Centre de Recherche en Informatique (CRI), MINES ParisTech - École nationale supérieure des mines de Paris, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Université Paris-Saclay, Frédéric Blanqui, Olivier Hermant, and Mines Paris - PSL (École nationale supérieure des mines de Paris)

Subjects
Polymorphisme d'univers, Rewriting, Type theory, Universe Polymorphism, Théorie des types, Réécriture, Eta-Conversion, Cadre logique, Logical Framework, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Termination, Terminaison
Abstract

Dedukti is a logical framework in which the user encodes the theory she wantsto use via rewriting rules. To ensure the decidability of typing, the rewriting system must be terminating.After recalling some properties of pure type systems and their extension with rewriting, a termination criterion for higher-order rewriting with dependent types is presented. It is an extension of the dependency pairs to the lambda-pi-calculus modulo rewriting. This result features two main theorems. The first one states that the well-foundedness of the call relation defined from dependency pairs implies the strong normalization of the rewriting system.The second result of this part describes decidable sufficient conditions to use the first one. This decidable version of the termination criterion is implemented in “SizeChange Tool”.The second part of this thesis is dedicated to the use of the logical framework Dedukti to encode a rich type theory. We are interested in a fragment of the logic beyond Agda which includes two widely used features: extension of conversion with the eta rule and universe polymorphism.Once again, this work includes a theoretical part, with correct encodings of both features in the lambda-pi-calculus modulo rewriting, and a prototypical translator from Agda to Dedukti.; Dedukti est un cadre logique dans lequel l’utilisateur encode la théorie qu’il souhaite utiliser à l’aide de règles de réécriture. Pour garantir la décidabilité du typage, il faut s’assurer que le système de réécriture utilisé est terminant.Après avoir rappelé les propriétés des systèmes de types purs et leur extension avec de la réécriture, un critère de terminaison pour la réécriture d’ordre supérieur avec types dépendants est présenté. Il s’agit d’une extension de la notion de paires de dépendances au cas du lambda-pi-calcul modulo réécriture. Cerésultat se décompose en deux théorèmes principaux. Le premier stipule que la bonne fondaison de la relation d’appel définie à partir des paires de dépendances implique la normalisation forte du système de réécriture.Le second résultat de cette partie décrit des conditions décidables suffisantes pour pouvoir utiliser le premier théorème. Cette version décidable du critère de terminaison est implémenté dans un outil appelé “SizeChange Tool”.La seconde partie de cette thèse est consacrée à l’utilisation du cadre logiqueDedukti pour encoder une théorie des types riche. Nous nous intéressons plusparticulièrement à la traduction d’un fragment d’Agda incluant deux fonctionnalités très répandues : l’extension de la conversion avec la règle eta et le polymorphisme d’univers.Une fois encore, ce travail possède un versant théorique, avec des encodagesprouvés corrects de ces deux fonctionnalités dans le lambda-pi-calcul modulo réécriture, ainsi qu’une implémentation prototypique de traducteur entre Agda et Dedukti.

Published
2020

42. Interopérabilité entre systèmes de preuve en utilisant le cadre logique Dedukti

Author

Thiré, François, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), ENS Paris-Saclay, Gilles Dowek, Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris-Saclay, Stéphane Lengrand, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], type systems, Lambdapi modulo theory, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], interoperability, Dedukti, Logical framework, systèmes de type, Matita, HOL-Light, interopérabilité, Coq, [INFO]Computer Science [cs], Interoperabilité, Cadre logique
Abstract

There is today a large family of proof systems based upon variouslogics: The Calculus of Inductive Constructions, Higher-Order logic orSet theory, etc. The diversity of proof systems has the negativeconsequence that theorems are formalized many times. One way toovercome this issue would be to make proof systems interoperable. Inthis thesis, we have tackled the interoperability problem for proofsystems both on the theoretical and the practical side using theDedukti logical framework.We begin our journey by looking at Cumulative Type Systems (CTS), afamily of type systems which extends that of Pure Type Systemswith a subtyping relation. CTS provides a common skeleton to manylogics used today. The logic behind Coq, HOL-Light, Lean, Matita orPVS can be seen as an extension of CTS with various features(inductive types, proof irrelevance, predicate subtyping, …). Wedefine a new notion of embedding between CTS. We also provide a soundbut incomplete algorithm to decide whether a proof in one CTS can betranslated into another CTS. This algorithm can also be seen as anextension of Coq's algorithm to check that the floating universeconstraints are consistent. Then, we propose a new embedding of CTSinto Dedukti and give a soundness proof of this embedding. Theseresults show that Dedukti is suitable for studying interoperability onthe theoretical side.We continue our journey on a case of study: The proof of Fermat'slittle theorem written in Matita. We show how we were able totranslate this proof to various proof systems through Dedukti. Thistranslation mainly relies on two tools created for this purpose:— Dkmeta, a tool which proposes to use rewriting as a way to writeproofs transformation programs. One advantage of this tool is that itreuses the syntax of Dedukti itself.— Universo, a tool which implements the aforementioned algorithm whichallows to translate a proof in one CTS (written in Dedukti) toanother.This semi-automatic translation allows to translate the proof ofFermat's little theorem into a weak but expressive logic calledSTTforall. STTforall is a constructive version of Simple Type Theorywith prenex polymorphism. As a consequence, a proof in STTforall canbe exported easily to many proof systems. This case of study showsthat Dedukti is also suitable for interoperability on the practicalside.The tools used for these transformations could be reused also forproofs coming from other proof systems for which an encoding inDedukti is known (such as Coq or Agda).The journey ends with the exportation of the proof of Fermat's littletheorem encoded in STTforall towards 5 different proof systems: Coq,Lean, Matita, OpenTheory (a member of the HOL-family proof systems)and PVS. We have implemented a user interface for that via a websitecalled Logipedia.Logipedia was designed with the goal of containing many more proofs thatcould be shared between proof systems and as such is intended to be anencyclopedia of formal proofs.; Il existe aujourd'hui une large famille de systèmes de preuve baséesur différentes logiques: Le calcul des constructions inductives, lalogique d'ordre supérieur, la théorie des ensembles, etc... Undésavantage majeur de cette diversité est, que les théorèmes sontprouvés de nombreuses fois. Une possibilité pour résoudre ce problèmeest de rendre les systèmes de preuve interoperables. Dans cette thèse,nous avons attaqué le problème d'interopérabilité entre systèmes depreuve aussi bien sur le plan théorique que le plan pratique enutilisant le cadre logique Dedukti.Notre voyage commence avec l'exploration des systèmes de typescumulatifs (CTS), une famille de systèmes de type qui étend celle dessystèmes de types pures avec une relation de sous-typage. Les CTSfournissent aujourd'hui une squelette commun a beaucoup de logiquesutilisés aujourd'hui. Les logiques derrières les systèmes Coq,HOL-Light, Lean, Matita ou bien PVS peuvent toutes être vues comme desextensions des CTS avec des fonctionnalités différentes (typesinductifs, irrelevance de la preuve, sous-typage propositionnel,...). Nous définissons une nouvelle notion de traduction entreCTS. Entre autre, nous expliquons un nouvel algorithme (correct maisincomplet) pour déterminer si une preuve écrite dans un CTS peut-êtretraduire dans un autre CTS. Cet algorithme peut aussi être vu commeune extension de l'algorithme de Coq qui permet de vérifier qu'unensemble de contraintes sur les univers est cohérent. Finalement, nousproposons un nouvel encodage des CTS dans Dedukti et nous prouvonsque cet encodage est correct. Ces résultats montrent que Dedukti estun cadre logique approprié sur le plan théorique pour étudierl'interopérabilité entre systèmes de preuve.Nous poursuivons notre voyage avec une étude de cas: le petit théorèmede Fermat prouvé en Matita. Nous montrons comment nous avons putraduire cette preuve vers différents systèmes à travers le cadrelogique Dedukti. Cette traduction se repose principalement sur deuxoutils que nous avons créees :- Dkmeta qui permet d'utiliser la réécriture comme un langage à partentière pour écrire des traductions de preuves. Un avantage de cetoutil est qu'il ré-utilise la syntaxe de Dedukti.- Universo, un outil qui permet d'implémenter l'algorithme mentionnéprécédemment qui permet de traduire une preuve d'un CTS (en Dedukti)vers un autre.Cette procédure semi-automatique permet de traduire la preuve du petitthéorème de Fermat dans une logique assez faible mais expressive quel'on appelle STTforall. STTforall est une version constructive de lathéorie des types simples avec du polymorphisme prénexe. La simplicitéde cette logique permet d'exporter des preuves de STTforall vers denombreux systèmes de preuve. Cette étude de cas montre que Deduktiest tout aussi efficace en tant qu'outil pour faire del'interopérabilité sur le plan pratique.Les outils que nous avons développés dans cette thèse ne sont passpécifiques à cette traduction et peuvent être réutilisés pourd'autres systèmes de preuve dont un encodage en Dedukti est connu(comme Coq ou bien Agda).Finalement, nous concluons ce voyage avec l'exportation du petitthéorème de Fermat vers cinq systèmes de preuve différents: Coq, Lean,Matita, OpenTheory (membre de la famille des systèmes de preuve basésur la logique d'ordre supérieure) et PVS. Cette traduction estdisponible via un site web appelé Logipedia.Logipedia n'a pas été créé seulement pour cette traduction mais avecl'objectif de contenir beaucoup plus de preuves que l'on pourraitpartager entre plusieurs systèmes de preuves. Cela rendrait Logipediaalors une encyclopédie de preuves formelles en ligne.

Published
2020

43. Importer les preuves de Logipedia dansAgda

Author

Delort, Tristan, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Inria Saclay Ile de France, and Frederic Blanqui

Subjects
[INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
Published
2020

44. A calculus of expandable stores

Author

Étienne Miquey, Hugo Herbelin, Design, study and implementation of languages for proofs and programs (PI.R2), Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Paris (UP)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP)-Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), Centre National de la Recherche Scientifique (CNRS), Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), The second author was supported by the Paris Ile-de-France Region, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
Global environment, 050101 languages & linguistics, Evaluation strategy, Computer science, System F, 05 social sciences, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 02 engineering and technology, Data type, Abstract machine, de Bruijn indices, Continuation, Control flow, If and only if, CPS translations, 0202 electrical engineering, electronic engineering, information engineering, Calculus, Lazy evaluation, 020201 artificial intelligence & image processing, 0501 psychology and cognitive sciences, CPS trans- lations, Kripke forcing, Abstract machines
Abstract

LICS 2020 will be held online; International audience; The call-by-need evaluation strategy for the λ-calculus is an evaluation strategy that lazily evaluates arguments only if needed, and if so, shares computations across all places where it is needed. To implement this evaluation strategy, abstract machines require some form of global environment. While abstract machines usually lead to a better understanding of the flow of control during the execution, facilitating in particular the definition of continuation-passing style translations , the case of machines with global environments turns out to be much more subtle. The main purpose of this paper is to understand how to type a continuation-and-environment-passing style translation , that is to say how to soundly translate in continuation-passing style a calculus with global environment. To this end, we introduce Fϒ , a generic calculus to define the target of such translations. In particular, Fϒ features a data type for typed stores and a mechanism of explicit coercions witnessing store extensions along environment-passing style translations. On the logical side, this broadly amounts to a Kripke forcing-like translation mixed with a negative translation (for the continuation-passing part). Since Fϒ allows for the definition of such translations for different source calculi (call-by-need, call-by-name, call-by-value) with different type systems (simple types, system F), we claim that it precisely captures the computational content of continuation-and-environment-passing style translations.

Published
2020
Full Text
View/download PDF

45. Encoding Agda Programs Using Rewriting

Author

Genestier, Guillaume, Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Université Paris-Saclay, Centre National de la Recherche Scientifique (CNRS), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Mines Paris - PSL (École nationale supérieure des mines de Paris), and Université Paris sciences et lettres (PSL)

Subjects
Logical Frameworks, Rewriting, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Eta Conversion, Universe Polymorphism, Theory of computation → Equational logic and rewriting, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Theory of computation → Type theory
Abstract

International audience; We present in this paper an encoding in an extension with rewriting of the Edimburgh Logical Framework (LF) [Harper et al., 1993] of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between Agda and Dedukti developped by the author.

Published
2020
Full Text
View/download PDF

46. The New Rewriting Engine of Dedukti

Author

Hondet, Gabriel, Blanqui, Frédéric, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Centre National de la Recherche Scientifique (CNRS), and Université Paris-Saclay

Subjects
Computer Science - Symbolic Computation, Rewriting algorithm, [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], Computer Science - Programming Languages, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, non-linear higher-order pattern matching
Abstract

International audience; Dedukti is a type-checker for the λΠ-calculus modulo rewriting, an extension of Edinburgh’s logicalframework LF where functions and type symbols can be defined by rewrite rules. It thereforecontains an engine for rewriting LF terms and types according to the rewrite rules given by the user.A key component of this engine is the matching algorithm to find which rules can be fired. In thispaper, we describe the class of rewrite rules supported by Dedukti and the new implementation ofthe matching algorithm. Dedukti supports non-linear rewrite rules on terms with binders usinghigher-order pattern-matching as in Combinatory Reduction Systems (CRS). The new matchingalgorithm extends the technique of decision trees introduced by Luc Maranget in the OCamlcompiler to this more general context.

Published
2020
Full Text
View/download PDF

47. Type safety of rewrite rules in dependent types

Author

Blanqui, Frédéric, Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Université Paris-Saclay, Centre National de la Recherche Scientifique (CNRS), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), and Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
Computer Science - Logic in Computer Science, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computer Science - Programming Languages, Rewriting Theory, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Dependent type theory, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], type preservation
Abstract

International audience; The expressiveness of dependent type theory can beextended by identifying types modulo some additional computation rules. But, forpreserving the decidability of type-checking or the logicalconsistency of the system, one must make sure that those user-definedrewriting rules preserve typing. In this paper, we give a newmethod to check that property using Knuth-Bendix completion.

Published
2020
Full Text
View/download PDF

48. Linking Focusing and Resolution with Selection

Author

Guillaume Burel, Méthodes et modèles pour les réseaux (METHODES-SAMOVAR), Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux (SAMOVAR), Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP)-Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Igor Potapov, Paul Spirakis, and James Worrell

Subjects
General Computer Science, Logic, Computer science, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory, Modulo, 02 engineering and technology, proof theory, Mathematical proof, 01 natural sciences, refinements of resolution, Theoretical Computer Science, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Calculus, Sequent, 0101 mathematics, automated deduction, 060201 languages & linguistics, polarization, 000 Computer science, knowledge, general works, 010102 general mathematics, Sequent calculus, Atomic formula, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 06 humanities and the arts, 16. Peace & justice, deduction modulo theory, Computational Mathematics, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, sequent calculus, Proof theory, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0602 languages and literature, Computer Science, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.4: Mechanical theorem proving, 020201 artificial intelligence & image processing, Rewriting
Abstract

Focusing and selection are techniques that shrink the proof-search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atomic formula can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory and the related framework called superdeduction; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof-search space.

Published
2020
Full Text
View/download PDF

49. The Algebra of Infinite Sequences: Notations and Formalization

Author

Dershowitz, Nachum, Jouannaud, Jean-Pierre, Wang, Qian, School of Computer Science (TAU-CS), Tel Aviv University (TAU), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Tsinghua University [Beijing] (THU), Tel Aviv University [Tel Aviv], and Jouannaud, Jean-Pierre

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ACM: D.: Software, ACM: F.: Theory of Computation
Abstract

We propose some convenient notations for expressing complicated properties of finite and infinite, ordinal-indexed sequences. The algebra of ordinal-indexed sequences is being implemented in the proof-assistant Coq, together with the algebra of ordinals represented in Cantor normal form. 1 Purpose In infinite combinatorics, program verification, and other subjects of mathematical interest, one often encounters a need to describe properties of finite and infinite sequences. For example, a "good" sequence in well-quasi-ordering (wqo) theory is an infinite sequence containing at least one element that is related (in a quasi-ordering) to a subsequent element. We have been seeking convenient notations and operations that would enable us to easily express properties of sequences that are of interest. Not finding anything suiting our needs, we propose some in this note. In programming and proof development, the idea of dependent types has established itself as most useful for various applications. In practice, such types depend either on natural numbers, such as lists depending on a natural number expressing their length, or on a proposition whose proof is required for type-checking purposes. Infinite lists, as studied in this note, will depend instead on ordinals. This paper therefore contains a formalization in Coq of ordinals in Cantor normal form, and their use for formalizing infinite sequences. Proofs of most statements are provided in the online supplement. 2 Finite Paths We begin with the simpler finite case. Let V be a (finite or infinite) alphabet, which we call points (akin to vertices), and let V n be all n-tuples of points, thought of as n-element sequences, which we refer to as paths. The length of a path s 0 , s 1 ,. .. , s n−1 is n, the number of its

Published
2020

50. Unification of drags

Author

Jouannaud, Jean-Pierre, Orejas, Fernando, Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and Universitat Politècnica de Catalunya [Barcelona] (UPC)

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ACM: D.: Software, ACM: F.: Theory of Computation, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

We develop unification for graph rewriting based on the drag model [8]. 1 Introduction Rewriting with graphs has a long history in computer science, graphs being used to represent data structures, but also program structures and even concurrent and distributed computational models. They therefore play a key rôle in program evaluation, transformation, and optimization, and more generally program analysis; see, for example, [2]. Our work is based on a recent, purely combinatorial view of graphs [8]. Drags are labelled graphs equipped with roots and sprouts. Roots are vertices without predecessors that can be seen as input ports, while sprouts are vertices without successors labelled by variables that can be seen as output ports. Drags appear as a generalization of terms which admit many roots, arbitrary sharing, and cycles. Rewrite rules are then pairs of drags that preserve variables and roots, hence avoiding the creation of dangling edges when rewriting. A key aspect of drags is that they can be equipped with a composition operator so that matching a left-hand side of rule L w.r.t. an input drag D amounts to write D as the composition of a context graph C with L, and rewriting D with the rule L → R amounts to replace L with R in that composition. Since substitutions cannot be separated from context in presence of cycles, composition must play both rôles of plugging a context and a substitution. To assess our claim that drags are a natural generalization of terms, it is our program to extend the most useful term rewriting techniques to drags. The recursive path ordering is extended in [7]. In this paper, we consider unification. First, we generalize the subsumption order to drags thanks to composition. Our main result is then unifiable drags admit a most general unifier which can be computed in quadratic time. Comparisons with the literature is addressed in Section 2. An interesting relationship between unification of drags and of rational dags is pointed out in conclusion.

Published
2020

Catalog

Books, media, physical & digital resources
See catalog results