2023
Journal articles
- titre
- Unification of Drags and Confluence of Drag Rewriting
- auteur
- Jean-Pierre Jouannaud, Fernando Orejas
- article
- Journal of Logical and Algebraic Methods in Programming, 2023, 131, pp.26. ⟨10.1016/j.jlamp.2022.100845⟩
- identifiant
- hal-02562152
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Traduire l'univers des mathématiques en Dedukti, sans univers
- auteur
- Amélie Ledein, Elliot Butte
- article
- JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.172-189
- identifiant
- hal-03936696
- Accès au texte intégral et bibtex
-
- titre
- Compositional pre-processing for automated reasoning in dependent type theory
- auteur
- Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial
- article
- CPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩
- identifiant
- hal-03901019
- Accès au texte intégral et bibtex
-
Reports
- titre
- Recommandations sur les « éditeurs de la zone grise »
- auteur
- Frédéric Blanqui, Anne Canteaut, Hidde de Jong, Sébastien Imperiale, Nathalie Mitton, Guillaume Pallez, Xavier Pennec, Xavier Rival, Bertrand Thirion
- article
- Inria. 2023, pp.1-3
- identifiant
- hal-04001505
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- On the convergence of reduction-based and model-based methods in proof theory
- auteur
- Gilles Dowek
- article
- 2023
- identifiant
- hal-04086043
- Accès au texte intégral et bibtex
-
- titre
- Correct and Complete Type Checking and Certified Erasure for Coq, in Coq
- auteur
- Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter
- article
- 2023
- identifiant
- hal-04077552
- Accès au texte intégral et bibtex
-
2022
Journal articles
- titre
- Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
- auteur
- Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu
- article
- Mathematical Structures in Computer Science, 2022, pp.1-36. ⟨10.1017/S0960129522000044⟩
- identifiant
- hal-03126111
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- From the Universality of Mathematical Truth to the Interoperability of Proof Systems
- auteur
- Gilles Dowek
- article
- IJCAR 2022 - International Joint Conference on Automated Reasoning, Aug 2022, Haifa, Israel. ⟨10.1007/978-3-031-10769-6_2⟩
- identifiant
- hal-03959359
- Accès au texte intégral et bibtex
-
- titre
- Adequate and Computational Encodings in the Logical Framework Dedukti
- auteur
- Thiago Felicissimo
- article
- FSCD 2022 - 7th International Conference on Formal Structures for Computation and Deduction, Aug 2022, Haifa, Israel. ⟨10.4230/LIPIcs.FSCD.2022.25⟩
- identifiant
- hal-03956666
- Accès au texte intégral et bibtex
-
- titre
- A direct computational interpretation of second-order arithmetic via update recursion
- auteur
- Valentin Blot
- article
- LICS 2022 - 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Aug 2022, Haïfa, Israel. ⟨10.1145/3531130.3532458⟩
- identifiant
- hal-03698879
- Accès au texte intégral et bibtex
-
- titre
- Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity
- auteur
- Frédéric Blanqui
- article
- FSCD 2022 - 7th International Conference on Formal Structures for Computation and Deduction, Aug 2022, Haifa, Israel. pp.14, ⟨10.4230/LIPIcs.FSCD.2022.24⟩
- identifiant
- hal-03708036
- Accès au bibtex
-
- titre
- Linear Lambda-Calculus is Linear
- auteur
- Alejandro Díaz-Caro, Gilles Dowek
- article
- FSCD 2022 - 7th International Conference on Formal Structures for Computation and Deduction, Tel Aviv University, Aug 2022, Haifa, Israel. ⟨10.4230/LIPIcs.FSCD.2022.21⟩
- identifiant
- hal-03959343
- Accès au texte intégral et bibtex
-
- titre
- An Implementation of Set Theory with Pointed Graphs in Dedukti
- auteur
- Valentin Blot, Gilles Dowek, Thomas Traversié
- article
- LFMTP 2022 - International Workshop on Logical Frameworks and Meta-Languages : Theory and Practice, Aug 2022, Haïfa, Israel
- identifiant
- hal-03740004
- Accès au texte intégral et bibtex
-
- titre
- Classical simulation of quantum circuits with partial and graphical stabiliser decompositions
- auteur
- Aleks Kissinger, Renaud Vilmart, John van de Wetering
- article
- 17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022), Jul 2022, Urbana-Champaign, United States. pp.5:1 - 5:13, ⟨10.4230/LIPIcs.TQC.2022.5⟩
- identifiant
- hal-03606226
- Accès au texte intégral et bibtex
-
- titre
- Vers une traduction de K en Dedukti
- auteur
- Amélie Ledein, Valentin Blot, Catherine Dubois
- article
- JFLA 2022 - Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France
- identifiant
- hal-03604962
- Accès au texte intégral et bibtex
-
- titre
- Bécassine à la chasse au Coq (démonstration)
- auteur
- Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial
- article
- JFLA 2022 - Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France
- identifiant
- hal-03604902
- Accès au texte intégral et bibtex
-
- titre
- Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
- auteur
- Michael Färber
- article
- 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’22), Jan 2022, Philadelphia, PA, United States. ⟨10.1145/3497775.3503683⟩
- identifiant
- hal-03143359
- Accès au texte intégral et bibtex
-
Lectures
- titre
- Proofs in theories
- auteur
- Gilles Dowek
- article
- Master. France. 2022, pp.154
- identifiant
- hal-04057037
- Accès au texte intégral et bibtex
-
Theses
- titre
- Expressing predicate subtyping in computational logical frameworks
- auteur
- Gabriel Hondet
- article
- Logic in Computer Science [cs.LO]. Université Paris-Saclay, 2022. English. ⟨NNT : 2022UPASG070⟩
- identifiant
- tel-03855351
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- A semantics of K into Dedukti
- auteur
- Amélie Ledein, Valentin Blot, Catherine Dubois
- article
- 2022
- identifiant
- hal-03895834
- Accès au texte intégral et bibtex
-
- titre
- Translating proofs from an impredicative type system to a predicative one
- auteur
- Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal
- article
- 2022
- identifiant
- hal-03848584
- Accès au texte intégral et bibtex
-
- titre
- A New Connective in Natural Deduction, and its Application to Quantum Computing ⋆
- auteur
- Alejandro Díaz-Caro, Gilles Dowek
- article
- 2022
- identifiant
- hal-03540150
- Accès au texte intégral et bibtex
-
- titre
- Explanation: from ethics to logic
- auteur
- Gilles Dowek
- article
- 2022
- identifiant
- hal-04055141
- Accès au texte intégral et bibtex
-
2021
Conference papers
- titre
- Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories
- auteur
- Gaspard Férey, Jean-Pierre Jouannaud
- article
- PPDP 2021 - 23rd International Symposium on Principles and Practice of Declarative Programming, Sep 2021, Tallin, Estonia. ⟨10.1145/3479394.3479403⟩
- identifiant
- hal-03126115
- Accès au texte intégral et bibtex
-
- titre
- Quantum Multiple-Valued Decision Diagrams in Graphical Calculi
- auteur
- Renaud Vilmart
- article
- MFCS 2021 - 46th International Symposium on Mathematical Foundations of Computer Science, Aug 2021, Tallinn, Estonia. pp.89:1--89:15, ⟨10.4230/LIPIcs.MFCS.2021.89⟩
- identifiant
- hal-03277262
- Accès au texte intégral et bibtex
-
- titre
- Some Axioms for Mathematics
- auteur
- Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
- article
- FSCD 2021 - 6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires / Virtual, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.20⟩
- identifiant
- hal-03279749
- Accès au texte intégral et bibtex
-
- titre
- General Automation in Coq through Modular Transformations
- auteur
- Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial
- article
- Seventh Workshop on Proof Exchange in Theorem Proving, Jul 2021, Pittsburgh, United States. ⟨10.4204/EPTCS.336.3⟩
- identifiant
- hal-03328935
- Accès au texte intégral et bibtex
-
- titre
- Geometry of Interaction for ZX-Diagrams
- auteur
- Kostia Chardonnet, Benoît Valiron, Renaud Vilmart
- article
- TLLA 2021 - 5th International Workshop on Trends in Linear Logic and Applications, Jun 2021, Rome / Virtual, Italy
- identifiant
- lirmm-03272411
- Accès au texte intégral et bibtex
-
Master thesis
- titre
- Representing Agda and coinduction in the λΠ-calculus modulo rewriting
- auteur
- Thiago Felicissimo
- article
- Logic in Computer Science [cs.LO]. 2021
- identifiant
- hal-03343699
- Accès au texte intégral et bibtex
-
Documents associated with scientific events
- titre
- Interacting Safely with an Unsafe Environment
- auteur
- Gilles Dowek
- article
- Logical Frameworks and Meta-Languages, 2021, Pittsburgh, United States. 337, pp.30 - 38, 2021, ⟨10.4204/eptcs.337.3⟩
- identifiant
- hal-03540149
- Accès au texte intégral et bibtex
-
Reports
- titre
- M1 Internship Report Translating proofs between Isabelle and Dedukti
- auteur
- Yann Leray
- article
- [Internship report] Deducteam - Inria Paris-Saclay / ENS Paris-Saclay. 2021
- identifiant
- hal-03348486
- Accès au texte intégral et bibtex
-
Theses
- titre
- Integrating Automated Theorem Provers in Proof Assistants
- auteur
- Yacine El Haddad
- article
- Automatic Control Engineering. Université Paris-Saclay, 2021. English. ⟨NNT : 2021UPASG052⟩
- identifiant
- tel-03387912
- Accès au texte intégral et bibtex
-
- titre
- Higher-Order Confluence and Universe Embedding in the Logical Framework
- auteur
- Gaspard Ferey
- article
- Other [cs.OH]. Université Paris-Saclay, 2021. English. ⟨NNT : 2021UPASG032⟩
- identifiant
- tel-03418761
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Confluence in UnTyped Higher-Order Theories by means of Critical Pairs
- auteur
- Gaspard Férey, Jean-Pierre Jouannaud
- article
- 2021
- identifiant
- hal-03126102
- Accès au texte intégral et bibtex
-
2020
Journal articles
- titre
- Linking Focusing and Resolution with Selection
- auteur
- Guillaume Burel
- article
- ACM Transactions on Computational Logic, 2020, 21 (3), pp.1-30. ⟨10.1145/3373276⟩
- identifiant
- hal-02908808
- Accès au texte intégral et bibtex
-
- titre
- First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice
- auteur
- Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant
- article
- Journal of Automated Reasoning, 2020, 64 (6), pp.1001-1050. ⟨10.1007/s10817-019-09533-z⟩
- identifiant
- hal-02305831
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- A calculus of expandable stores
- auteur
- Hugo Herbelin, Étienne Miquey
- article
- LICS 2020 - 35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken / Virtual, Germany. pp.564-577, ⟨10.1145/3373718.3394792⟩
- identifiant
- hal-02557823
- Accès au texte intégral et bibtex
-
- titre
- The New Rewriting Engine of Dedukti
- auteur
- Gabriel Hondet, Frédéric Blanqui
- article
- FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.16, ⟨10.4230/LIPIcs.FSCD.2020.35⟩
- identifiant
- hal-02981561
- Accès au texte intégral et bibtex
-
- titre
- Encoding Agda Programs Using Rewriting
- auteur
- Guillaume Genestier
- article
- FSCD - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. ⟨10.4230/LIPIcs.FSCD.2020.31⟩
- identifiant
- hal-03838613
- Accès au texte intégral et bibtex
-
- titre
- Type safety of rewrite rules in dependent types
- auteur
- Frédéric Blanqui
- article
- FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.14, ⟨10.4230/LIPIcs.FSCD.2020.13⟩
- identifiant
- hal-02981528
- Accès au texte intégral et bibtex
-
- titre
- Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory
- auteur
- Bruno Barras, Valentin Maestracci
- article
- LFMPT 2020 - Logical Frameworks and Meta-Languages: Theory and Practice 2020, Jun 2020, Paris, France
- identifiant
- hal-03138145
- Accès au texte intégral et bibtex
-
- titre
- Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory
- auteur
- Gabriel Hondet, Frédéric Blanqui
- article
- TYPES 2020 - 26th International Conference on Types for Proofs and Programs, Mar 2020, Turino, Italy. ⟨10.4230/LIPIcs.TYPES.2020.6⟩
- identifiant
- hal-03279766
- Accès au texte intégral et bibtex
-
Book sections
- titre
- Theoretical Computer Science: Computability, Decidability and Logic
- auteur
- Olivier Bournez, Gilles Dowek, Rémi Gilleron, Serge Grigorieff, Jean-Yves Marion, Simon Perdrix, S. Tison
- article
- A Guided Tour of Artificial Intelligence Research - Volume III: Interfaces and Applications of Artificial Intelligence (10.1007/978-3-030-06170-8), Springer International Publishing, pp.1-50, 2020, ⟨10.1007/978-3-030-06170-8_1⟩
- identifiant
- hal-03173193
- Accès au bibtex
-
- titre
- Theoretical Computer Science: Computational Complexity
- auteur
- Olivier Bournez, Gilles Dowek, Rémi Gilleron, Serge Grigorieff, Jean-Yves Marion, Simon Perdrix, S. Tison
- article
- A Guided Tour of Artificial Intelligence Research - Volume III: Interfaces and Applications of Artificial Intelligence (10.1007/978-3-030-06170-8), Springer International Publishing, 2020
- identifiant
- hal-02995771
- Accès au bibtex
-
Master thesis
- titre
- Importer les preuves de Logipedia dans Agda
- auteur
- Tristan Delort
- article
- Théorie et langage formel [cs.FL]. 2020
- identifiant
- hal-02985530
- Accès au texte intégral et bibtex
-
Theses
- titre
- Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting
- auteur
- Guillaume Genestier
- article
- Computation and Language [cs.CL]. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG045⟩
- identifiant
- tel-03167579
- Accès au texte intégral et bibtex
-
- titre
- Interoperability between proof systems using the logical framework Dedukti
- auteur
- François Thiré
- article
- Programming Languages [cs.PL]. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG053⟩
- identifiant
- tel-03224039
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- The Algebra of Infinite Sequences: Notations and Formalization
- auteur
- Nachum Dershowitz, Jean-Pierre Jouannaud, Qian Wang
- article
- 2020
- identifiant
- hal-02569232
- Accès au texte intégral et bibtex
-
- titre
- Les réseaux condition nécessaire du confinement et nouvel outil de santé publique
- auteur
- Gilles Dowek
- article
- 2020
- identifiant
- hal-04054797
- Accès au texte intégral et bibtex
-
- titre
- Logipedia: a multi-system encyclopedia of formal proofs
- auteur
- Gilles Dowek, François Thiré
- article
- 2020
- identifiant
- hal-04060141
- Accès au texte intégral et bibtex
-
2019
Journal articles
- titre
- Drags: A Compositional Algebraic Framework for Graph Rewriting
- auteur
- Nachum Dershowitz, Jean-Pierre Jouannaud
- article
- Theoretical Computer Science, 2019, 777, pp.204-231. ⟨10.1016/j.tcs.2019.01.029⟩
- identifiant
- hal-03139788
- Accès au texte intégral et bibtex
-
- titre
- Two linearities for quantum computing in the lambda calculus ✩,✩✩
- auteur
- Alejandro Díaz-Caro, Gilles Dowek, Juan Pablo Rinaldi
- article
- BioSystems, 2019
- identifiant
- hal-02909128
- Accès au texte intégral et bibtex
-
- titre
- Towards Combining Model Checking and Proof Checking
- auteur
- Ying Jiang, Jian Liu, Gilles Dowek, Kailiang Ji
- article
- The Computer Journal, In press, ⟨10.1093/comjnl/bxy112⟩
- identifiant
- hal-01970274
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Ekstrakto A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
- auteur
- Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui
- article
- PxTP 2019 - Sixth Workshop on Proof eXchange for Theorem Proving, Aug 2019, Natal, Brazil. pp.27-35, ⟨10.4204/EPTCS.301.5⟩
- identifiant
- hal-02200548
- Accès au texte intégral et bibtex
-
- titre
- SizeChangeTool: A Termination Checker for Rewriting Dependent Types
- auteur
- Guillaume Genestier
- article
- HOR 2019 - 10th International Workshop on Higher-Order Rewriting, Jun 2019, Dortmund, Germany. pp.14-19
- identifiant
- hal-02442465
- Accès au texte intégral et bibtex
-
- titre
- Logipedia : vers un Wikipedia des démonstrations formelles
- auteur
- Gilles Dowek
- article
- Séminaire du LIRIMA, Jun 2019, Rennes, France
- identifiant
- hal-03584021
- Accès au bibtex
-
- titre
- Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
- auteur
- Frédéric Blanqui, Guillaume Genestier, Olivier Hermant
- article
- FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨10.4230/LIPIcs.FSCD.2019.9⟩
- identifiant
- hal-01943941
- Accès au texte intégral et bibtex
-
- titre
- Proof Normalisation in a Logic Identifying Isomorphic Propositions
- auteur
- Alejandro Díaz-Caro, Gilles Dowek
- article
- FSCD 2019 - International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany
- identifiant
- hal-02909135
- Accès au texte intégral et bibtex
-
- titre
- Cumulative Types Systems and Levels
- auteur
- François Thiré
- article
- LFMTP 2019 - Logical Frameworks and Meta-Languages: Theory and Practice, Jun 2019, Vancouver, Canada
- identifiant
- hal-02150179
- Accès au texte intégral et bibtex
-
- titre
- Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
- auteur
- Frédéric Blanqui, Guillaume Genestier, Olivier Hermant
- article
- TYPES 2019 - 25th International Conference on Types for Proofs and Programs, Jun 2019, Oslo, Norway. pp.30-31
- identifiant
- hal-02442484
- Accès au texte intégral et bibtex
-
- titre
- Unboxing Mutually Recursive Type Definitions in OCaml
- auteur
- Simon Colin, Rodolphe Lepigre, Gabriel Scherer
- article
- JFLA 2019 - 30 èmes journées francophones des langages applicatifs, Jan 2019, Les Rousses, France
- identifiant
- hal-01929508
- Accès au texte intégral et bibtex
-
Master thesis
- titre
- Checking the type safety of rewrite rules in the $λΠ$-calculus modulo rewriting
- auteur
- Jui-Hsuan Wu
- article
- Computer Science [cs]. 2019
- identifiant
- hal-02288720
- Accès au texte intégral et bibtex
-
- titre
- Efficient rewriting using decision trees
- auteur
- Gabriel Hondet
- article
- Logic in Computer Science [cs.LO]. 2019
- identifiant
- hal-02317471
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Confluence in (Un)Typed Higher-Order Theories by means of Critical Pairs
- auteur
- Gaspard Ferey, Jean-Pierre Jouannaud
- article
- 2019
- identifiant
- hal-02096540
- Accès au texte intégral et bibtex
-
- titre
- Verifiable certificates for predicate subtyping
- auteur
- Frédéric Gilbert
- article
- 2019
- identifiant
- hal-01977585
- Accès au texte intégral et bibtex
-
- titre
- Two consequences of the hypothesis that we are within the world
- auteur
- Gilles Dowek
- article
- 2019
- identifiant
- hal-04055137
- Accès au texte intégral et bibtex
-
- titre
- Instinct, language, and artificial intelligence
- auteur
- Gilles Dowek
- article
- 2019
- identifiant
- hal-04054594
- Accès au texte intégral et bibtex
-
- titre
- How the physical Church-Turing thesis changed the concept of machine
- auteur
- Gilles Dowek
- article
- 2019
- identifiant
- hal-04054606
- Accès au texte intégral et bibtex
-
2018
Journal articles
- titre
- Abstract Representation of Binders in OCaml using the Bindlib Library
- auteur
- Rodolphe Lepigre, Christophe Raffalli
- article
- Electronic Proceedings in Theoretical Computer Science, 2018, 274, pp.42-56. ⟨10.4204/EPTCS.274.4⟩
- identifiant
- hal-01972050
- Accès au bibtex
-
- titre
- Sharing a Library between Proof Assistants: Reaching out to the HOL Family *
- auteur
- François Thiré
- article
- Electronic Proceedings in Theoretical Computer Science, 2018, 274, pp.57 - 71. ⟨10.4204/EPTCS.274.5⟩
- identifiant
- hal-01929714
- Accès au texte intégral et bibtex
-
- titre
- Size-based termination of higher-order rewriting
- auteur
- Frédéric Blanqui
- article
- Journal of Functional Programming, 2018, ⟨10.1017/S0956796818000072⟩
- identifiant
- hal-01424921
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Graph Path Orderings
- auteur
- Nachum Dershowitz, Jean-Pierre Jouannaud
- article
- 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2018, Awassa, Ethiopia. pp.1-18
- identifiant
- hal-01903086
- Accès au texte intégral et bibtex
-
- titre
- Linking Focusing and Resolution with Selection
- auteur
- Guillaume Burel
- article
- 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018), Aug 2018, Liverpool, United Kingdom. pp.9:1-9:14, ⟨10.4230/LIPIcs.MFCS.2018.9⟩
- identifiant
- hal-01670476
- Accès au texte intégral et bibtex
-
- titre
- Termination of λΠ modulo rewriting using the size-change principle (work in progress)
- auteur
- Frédéric Blanqui, Guillaume Genestier
- article
- 16th International Workshop on Termination, Jul 2018, Oxford, United Kingdom. pp. 10-14
- identifiant
- hal-01944731
- Accès au texte intégral et bibtex
-
- titre
- Drags: A Simple Algebraic Framework For Graph Rewriting
- auteur
- Nachum Dershowitz, Jean-Pierre Jouannaud
- article
- TERMGRAPH 2018 - 10th International Workshop on Computing with Terms and Graphs, Jul 2018, Oxford, United Kingdom
- identifiant
- hal-01853836
- Accès au texte intégral et bibtex
-
Master thesis
- titre
- Industrial Placement Report Research Placement in Deducteam
- auteur
- Aristomenis-Dionysios Papadopoulos
- article
- Logic in Computer Science [cs.LO]. 2018
- identifiant
- hal-01890253
- Accès au texte intégral et bibtex
-
- titre
- Une interface pour Dedukti
- auteur
- Ismaïl Lachheb
- article
- Informatique [cs]. 2018
- identifiant
- hal-01898401
- Accès au texte intégral et bibtex
-
- titre
- Encyclopédie en ligne de démonstrations formelles
- auteur
- Walid Moustaoui
- article
- Logique en informatique [cs.LO]. 2018
- identifiant
- hal-01975446
- Accès au texte intégral et bibtex
-
Reports
- titre
- Comparaison des termes avec partage
- auteur
- Quentin Ye
- article
- [Rapport de recherche] LSV, ENS Cachan, CNRS, INRIA, Université Paris-Saclay, Cachan (France). 2018
- identifiant
- hal-01973539
- Accès au texte intégral et bibtex
-
Theses
- titre
- Extending higher-order logic with predicate subtyping
- auteur
- Frédéric Gilbert
- article
- Logic in Computer Science [cs.LO]. Université Sorbonne Paris Cité; Université Paris Diderot, 2018. English. ⟨NNT : ⟩
- identifiant
- hal-01673518
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- A logic identifying isomorphic propositions
- auteur
- Alejandro Díaz-Caro, Gilles Dowek
- article
- 2018
- identifiant
- hal-01109104
- Accès au texte intégral et bibtex
-
- titre
- Execution traces and reduction sequences
- auteur
- Gilles Dowek
- article
- 2018
- identifiant
- hal-04060154
- Accès au texte intégral et bibtex
-
2017
Journal articles
- titre
- Rules and derivations in an elementary logic course
- auteur
- Gilles Dowek
- article
- IfColog Journal of Logics and their Applications (FLAP), 2017, 4 (1)
- identifiant
- hal-01252124
- Accès au texte intégral et bibtex
-
- titre
- Quantum causal graph dynamics
- auteur
- Pablo Arrighi, Simon Martiel
- article
- Physical Review D, 2017, 96 (2), pp.024026
- identifiant
- hal-01785461
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Typing Quantum Superpositions and Measurement
- auteur
- Alejandro Díaz-Caro, Gilles Dowek
- article
- TPNC 2017 - 6th International Conference on the Theory and Practice of Natural Computing, Dec 2017, Prague, Czech Republic. pp.13, ⟨10.1007/978-3-319-71069-3_22⟩
- identifiant
- hal-01670387
- Accès au texte intégral et bibtex
-
- titre
- Proof certificates in PVS
- auteur
- Frédéric Gilbert
- article
- ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. pp.262-268, ⟨10.1007/978-3-319-66107-0_17⟩
- identifiant
- hal-01673517
- Accès au texte intégral et bibtex
-
- titre
- Analyzing individual proofs as the basis of interoperability between proof systems
- auteur
- Gilles Dowek
- article
- PxTP 2017 - Fifth Workshop on Proof eXchange for Theorem Proving, Sep 2017, Brasilia, Brazil
- identifiant
- hal-01670394
- Accès au texte intégral et bibtex
-
- titre
- PML 2 : Integrated Program Verification in ML
- auteur
- Rodolphe Lepigre
- article
- 23rd International Conference on Types for Proofs and Programs (TYPES 2017), Jul 2017, Budapest, Hungary. pp.27, ⟨10.4230/LIPIcs.TYPES.2017.5⟩
- identifiant
- hal-01972000
- Accès au texte intégral et bibtex
-
- titre
- Coq without Type Casts: A Complete Proof of Coq Modulo Theory
- auteur
- Jean-Pierre Jouannaud, Pierre-Yves Strub
- article
- LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, May 2017, Maun, Botswana
- identifiant
- hal-01664457
- Accès au texte intégral et bibtex
-
- titre
- Automated Constructivization of Proofs
- auteur
- Frédéric Gilbert
- article
- FoSSaCS 2017, Apr 2017, Uppsala, Sweden. ⟨10.1007/978-3-662-54458-7_28⟩
- identifiant
- hal-01516788
- Accès au texte intégral et bibtex
-
Master thesis
- titre
- Termination checking in the λΠ-calculus modulo theory. From a practical and a theoretical viewpoint
- auteur
- Guillaume Genestier
- article
- Logic in Computer Science [cs.LO]. 2017
- identifiant
- hal-01676409
- Accès au texte intégral et bibtex
-
- titre
- Tactiques de preuve dans Dedukti
- auteur
- Antoine Defourné
- article
- Logique en informatique [cs.LO]. 2017
- identifiant
- hal-01661872
- Accès au texte intégral et bibtex
-
Books
- titre
- Le temps des algorithmes
- auteur
- Serge Abiteboul, Gilles Dowek
- article
- Editions Le Pommier, pp.192, 2017, 978-2746511750
- identifiant
- hal-01502505
- Accès au bibtex
-
Poster communications
- titre
- mSAT:An OCaml SAT Solver
- auteur
- Guillaume Bury
- article
- OCaml Users and Developers Workshop, Sep 2017, Oxford, United Kingdom
- identifiant
- hal-01670765
- Accès au texte intégral et bibtex
-
- titre
- Interoperability between arithmetic proofs using Dedukti
- auteur
- Gilles Dowek, Stéphane Graham-Lengrand, François Thiré
- article
- International School On Rewriting 2017, Jul 2017, Eindhoven, Netherlands
- identifiant
- hal-01668246
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Exporting an Arithmetic Library from Dedukti to HOL
- auteur
- François Thiré
- article
- 2017
- identifiant
- hal-01668250
- Accès au texte intégral et bibtex
-
- titre
- Models and termination of proof reduction in the λΠ-calculus modulo theory
- auteur
- Gilles Dowek
- article
- 2017
- identifiant
- hal-01101834
- Accès au texte intégral et bibtex
-
- titre
- Untyped Confluence In Dependent Type Theories
- auteur
- Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu
- article
- 2017
- identifiant
- hal-01515505
- Accès au texte intégral et bibtex
-
2016
Journal articles
- titre
- Toward the Rational Design of Galactosylated Glycoclusters That Target Pseudomonas aeruginosa Lectin A (LecA): Influence of Linker Arms That Lead to Low-Nanomolar Multivalent Ligands
- auteur
- Shuai Wang, Lucie Dupin, Mathieu Noël, Cindy Carroux, Louis Renaud, Thomas Gehin, Albert Meyer, Eliane Souteyrand, Jean-Jacques Vasseur, Gérard Vergoten, Yann Chevolot, François Morvan, Sébastien Vidal
- article
- Chemistry - A European Journal, 2016, 22 (33), pp.11785-11794. ⟨10.1002/chem.201602047⟩
- identifiant
- hal-02116180
- Accès au bibtex
-
- titre
- Free fall and cellular automata
- auteur
- Pablo Arrighi, Gilles Dowek
- article
- Electronic Proceedings in Theoretical Computer Science, 2016, 204, pp.1 - 10. ⟨10.4204/EPTCS.204.1⟩
- identifiant
- hal-01421712
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Soundly Proving B Method Formulae Using Typed Sequent Calculus
- auteur
- Pierre Halmagrand
- article
- 13th International Colloquium on Theoretical Aspects of Computing (ICTAC), Oct 2016, Taipei, Taiwan. pp 196-213, ⟨10.1007/978-3-319-46750-4_12⟩
- identifiant
- hal-01342849
- Accès au texte intégral et bibtex
-
- titre
- ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti
- auteur
- Raphaël Cauderlier, Catherine Dubois
- article
- ICTAC 2016 - 13th International Colloquium on Theoretical Aspects of Computing, Oct 2016, Taipei, Taiwan. pp.459-468, ⟨10.1007/978-3-319-46750-4_26⟩
- identifiant
- hal-01420638
- Accès au texte intégral et bibtex
-
- titre
- Resolution in Solving Graph Problems
- auteur
- Kailiang Ji
- article
- 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Jul 2016, Toronto, Canada
- identifiant
- hal-01245138
- Accès au texte intégral et bibtex
-
- titre
- Encoding Proofs in Dedukti: the case of Coq proofs
- auteur
- Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu
- article
- Proceedings Hammers for Type Theories, Jul 2016, Coimbra, Portugal
- identifiant
- hal-01330980
- Accès au texte intégral et bibtex
-
- titre
- Reversible Causal Graph Dynamics
- auteur
- Pablo Arrighi, Simon Martiel, Simon Perdrix
- article
- Reversible Computation, Jul 2016, Bologna, Italy. pp.73-88, ⟨10.1007/978-3-319-40578-0_5⟩
- identifiant
- hal-01361427
- Accès au bibtex
-
- titre
- Untyped Confluence in Dependent Type Theories
- auteur
- Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu
- article
- Proceedings Higher-Order Rewriting Workshop, Jun 2016, Porto, Portugal
- identifiant
- hal-01330955
- Accès au texte intégral et bibtex
-
- titre
- A Rewrite System for Proof Constructivization
- auteur
- Raphaël Cauderlier
- article
- Workshop on Logical Frameworks and Meta-Languages: Theory and Practice 2016, Jun 2016, Porto, Portugal. pp.1 - 7, ⟨10.1145/2966268.2966270⟩
- identifiant
- hal-01420634
- Accès au texte intégral et bibtex
-
- titre
- Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system
- auteur
- Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard
- article
- TYPES: Types for Proofs and Programs, May 2016, Novi SAd, Serbia
- identifiant
- hal-01441751
- Accès au texte intégral et bibtex
-
- titre
- Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval
- auteur
- Shuai Wang
- article
- AITP 2016 - Conference on Artificial Intelligence and Theorem Proving, Apr 2016, Obergurgl, Austria
- identifiant
- hal-01250197
- Accès au texte intégral et bibtex
-
Master thesis
- titre
- Internship report MPRI 2 Reverse engineering on arithmetic proofs
- auteur
- François Thiré
- article
- Computer Science [cs]. 2016
- identifiant
- hal-01424816
- Accès au texte intégral et bibtex
-
Theses
- titre
- Automated Deduction and Proof Certification for the B Method
- auteur
- Pierre Halmagrand
- article
- Logic in Computer Science [cs.LO]. Conservatoire National Des Arts et Métiers, Paris, 2016. English. ⟨NNT : ⟩
- identifiant
- tel-01420460
- Accès au texte intégral et bibtex
-
- titre
- Object-Oriented Mechanisms for Interoperability between Proof Systems
- auteur
- Raphaël Cauderlier
- article
- Logic in Computer Science [cs.LO]. Conservatoire National Des Arts et Métiers, Paris, 2016. English. ⟨NNT : ⟩
- identifiant
- tel-01415945
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- What is the Planck constant the magnitude of?
- auteur
- Pablo Arrighi, Gilles Dowek
- article
- 2016
- identifiant
- hal-01421711
- Accès au texte intégral et bibtex
-
- titre
- Automata, Resolution, and Cut-elimination
- auteur
- Guillaume Burel, Gilles Dowek, Ying Jiang
- article
- 2016
- identifiant
- hal-04063102
- Accès au texte intégral et bibtex
-
2015
Journal articles
- titre
- Termination of rewrite relations on λ-terms based on Girard's notion of reducibility
- auteur
- Frédéric Blanqui
- article
- Theoretical Computer Science, 2015, 611 (50-86), pp.37. ⟨10.1016/j.tcs.2015.07.045⟩
- identifiant
- hal-01191693
- Accès au texte intégral et bibtex
-
- titre
- The Computability Path Ordering
- auteur
- Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
- article
- Logical Methods in Computer Science, 2015, ⟨10.2168/LMCS-11(4:3)2015⟩
- identifiant
- hal-01163091
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Discrete Geodesics and Cellular Automata
- auteur
- Pablo Arrighi, Gilles Dowek
- article
- Theory and Practice of Natural Computing, Dec 2015, Mieres, Spain. ⟨10.1007/978-3-319-26841-5_11⟩
- identifiant
- hal-01252131
- Accès au texte intégral et bibtex
-
- titre
- A Lightweight Double-negation Translation
- auteur
- Frédéric Gilbert
- article
- LPAR-20. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji
- identifiant
- hal-01245021
- Accès au texte intégral et bibtex
-
- titre
- Normalization by Completeness with Heyting Algebras
- auteur
- Gaëtan Gilbert, Olivier Hermant
- article
- LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji
- identifiant
- hal-01204599
- Accès au texte intégral et bibtex
-
- titre
- Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
- auteur
- Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant
- article
- LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp 42-58
- identifiant
- hal-01204701
- Accès au texte intégral et bibtex
-
- titre
- Decidability, Introduction Rules and Automata
- auteur
- Gilles Dowek, Ying Jiang
- article
- International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Bula, Fiji. ⟨10.1007/978-3-662-48899-7_8⟩
- identifiant
- hal-01252135
- Accès au texte intégral et bibtex
-
- titre
- Implementing Polymorphism in Zenon
- auteur
- Guillaume Bury, Raphaël Cauderlier, Pierre Halmagrand
- article
- 11th International Workshop on the Implementation of Logics (IWIL), Nov 2015, Suva, Fiji
- identifiant
- hal-01243593
- Accès au texte intégral et bibtex
-
- titre
- A Completion Method to Decide Reachability in Rewrite Systems
- auteur
- Guillaume Burel, Gilles Dowek, Ying Jiang
- article
- International Symposium on Frontiers of Combining Systems FroCoS'15, Sep 2015, Wroclaw, Poland. pp.205-219, ⟨10.1007/978-3-319-24246-0_13⟩
- identifiant
- hal-01252138
- Accès au texte intégral et bibtex
-
- titre
- Confluence of layered rewrite systems
- auteur
- Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa
- article
- 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), Sep 2015, Berlin, Germany. pp.423--440, ⟨10.4230/LIPIcs.CSL.2015.423⟩
- identifiant
- hal-01199062
- Accès au texte intégral et bibtex
-
- titre
- Translating HOL to Dedukti
- auteur
- Ali Assaf, Guillaume Burel
- article
- Fourth Workshop on Proof eXchange for Theorem Proving, PxTP'15, Aug 2015, Berlin, Germany. pp.74-88, ⟨10.4204/EPTCS.186.8⟩
- identifiant
- hal-01097412
- Accès au texte intégral et bibtex
-
- titre
- Checking Zenon Modulo Proofs in Dedukti
- auteur
- Raphaël Cauderlier, Pierre Halmagrand
- article
- Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Aug 2015, Berlin, Germany
- identifiant
- hal-01171360
- Accès au texte intégral et bibtex
-
- titre
- Rewriting Modulo β in the λ Π-Calculus Modulo
- auteur
- Ronan Saillard
- article
- Logical Frameworks and Meta Languages: Theory and Practic, Affiliated with CADE-25, Aug 2015, Berlin, Germany. pp 87-101, ⟨10.4204/EPTCS.185.6⟩
- identifiant
- hal-01176715
- Accès au texte intégral et bibtex
-
- titre
- CTL Model Checking in Deduction Modulo
- auteur
- Kailiang Ji
- article
- Automated Deduction - CADE-25, Aug 2015, Berlin, Germany. pp 295-310, ⟨10.1007/978-3-319-21401-6_20⟩
- identifiant
- hal-01241132
- Accès au texte intégral et bibtex
-
- titre
- Médiation en sciences du numériques : un levier pour comprendre notre quotidien ?
- auteur
- Sylvie Alayrangues, Gilles Dowek, Erwan Kerrien, Jean Mairesse, Thierry Viéville
- article
- Science & You, Jun 2015, Nancy, France
- identifiant
- hal-01211457
- Accès au texte intégral et bibtex
-
Book sections
- titre
- On the definition of the classical connectives and quantifiers
- auteur
- Gilles Dowek
- article
- Edward Hermann Haeusler; Wagner de Campos Sanz; Bruno Lopes. Why is this a Proof?, Festschrift for Luiz Carlos Pereira , College Publications, 2015
- identifiant
- hal-01252221
- Accès au texte intégral et bibtex
-
Theses
- titre
- Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable.
- auteur
- Bruno Bernardo
- article
- Langage de programmation [cs.PL]. École polytechnique, 2015. Français. ⟨NNT : ⟩
- identifiant
- tel-01197380
- Accès au texte intégral et bibtex
-
- titre
- A framework for defining computational higher-order logics
- auteur
- Ali Assaf
- article
- Computer Science [cs]. École polytechnique, 2015. English. ⟨NNT : ⟩
- identifiant
- tel-01235303
- Accès au texte intégral et bibtex
-
- titre
- Model Checking and Theorem Proving
- auteur
- Kailiang Ji
- article
- Computation and Language [cs.CL]. Paris Diderot, 2015. English. ⟨NNT : ⟩
- identifiant
- tel-01251073
- Accès au texte intégral et bibtex
-
- titre
- Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond
- auteur
- Simon Cruanes
- article
- Logic in Computer Science [cs.LO]. École polytechnique, 2015. English. ⟨NNT : ⟩
- identifiant
- tel-01223502
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Objects and subtyping in the λΠ-calculus modulo
- auteur
- Raphaël Cauderlier, Catherine Dubois
- article
- 2015
- identifiant
- hal-01097444
- Accès au texte intégral et bibtex
-
- titre
- Cut-elimination and the decidability of reachability in alternating pushdown systems
- auteur
- Gilles Dowek, Ying Jiang
- article
- 2015
- identifiant
- hal-01101835
- Accès au texte intégral et bibtex
-
- titre
- Mixing HOL and Coq in Dedukti (Rough Diamond)
- auteur
- Ali Assaf, Raphaël Cauderlier
- article
- 2015
- identifiant
- hal-01141789
- Accès au texte intégral et bibtex
-
- titre
- Conservativity of embeddings in the lambda-Pi calculus modulo rewriting (long version)
- auteur
- Ali Assaf
- article
- 2015
- identifiant
- hal-01084165
- Accès au texte intégral et bibtex
-
- titre
- On the truth judgments in informatics
- auteur
- Gilles Dowek
- article
- 2015
- identifiant
- hal-04051523
- Accès au texte intégral et bibtex
-
2014
Journal articles
- titre
- Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
- auteur
- Ali Assaf, Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson, Benoît Valiron
- article
- Logical Methods in Computer Science, 2014, 10:4 (8), pp.40. ⟨10.2168/LMCS-10(4:8)2014⟩
- identifiant
- hal-01097602
- Accès au bibtex
-
Conference papers
- titre
- Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
- auteur
- Simon Cruanes
- article
- 4th Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienna, Austria
- identifiant
- hal-01101057
- Accès au texte intégral et bibtex
-
- titre
- Deduction modulo theory
- auteur
- Gilles Dowek
- article
- All about proofs. Proofs for all., Jul 2014, Wien, Austria
- identifiant
- hal-01101829
- Accès au texte intégral et bibtex
-
- titre
- Cut Admissibility by Saturation
- auteur
- Guillaume Burel
- article
- Joint International Conference, RTA-TLCA 2014, Jul 2014, Vienna, Austria. pp.124-138, ⟨10.1007/978-3-319-08918-8_9⟩
- identifiant
- hal-01097428
- Accès au texte intégral et bibtex
-
- titre
- Using Deduction Modulo in Set Theory
- auteur
- Pierre Halmagrand
- article
- SETS14, 1st International Workshop about Sets and Tools, Jun 2014, Toulouse, France. pp.12
- identifiant
- hal-01100512
- Accès au texte intégral et bibtex
-
- titre
- A calculus of constructions with explicit subtyping
- auteur
- Ali Assaf
- article
- 20th International Conference on Types for Proofs and Programs (TYPES 2014), May 2014, Institut Henri Poincaré, Paris, France
- identifiant
- hal-01097401
- Accès au texte intégral et bibtex
-
- titre
- Objects and subtyping in the lambda-Pi-calculus modulo
- auteur
- Raphaël Cauderlier, Ali Assaf, Catherine Dubois
- article
- TYPES 2014, May 2014, Paris, France. pp.2
- identifiant
- hal-01126394
- Accès au bibtex
-
Poster communications
- titre
- Dedukti : un vérificateur de preuves universel
- auteur
- Ronan Saillard
- article
- Journées de seconde année de l'Ecole Doctorale à Mines ParisTech, Jun 2014, Paris, France
- identifiant
- hal-01100519
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- A point on fixpoints in posets
- auteur
- Frédéric Blanqui
- article
- 2014
- identifiant
- hal-01097809
- Accès au texte intégral et bibtex
-
- titre
- A Logical Approach to CTL
- auteur
- Gilles Dowek, Ying Jiang
- article
- 2014
- identifiant
- hal-00919467
- Accès au texte intégral et bibtex
-
- titre
- Axiomatizing truth in a finite model
- auteur
- Gilles Dowek, Ying Jiang
- article
- 2014
- identifiant
- hal-00919469
- Accès au texte intégral et bibtex
-
- titre
- La notion de nombre réel : une solution simplexe ?
- auteur
- Gilles Dowek
- article
- 2014
- identifiant
- hal-04055835
- Accès au texte intégral et bibtex
-
2013
Journal articles
- titre
- A Formal Proof of Square Root and Division Elimination in Embedded Programs
- auteur
- Pierre Neron
- article
- Journal of Formalized Reasoning, 2013, 6 (1), pp.89-111
- identifiant
- hal-00924367
- Accès au texte intégral et bibtex
-
- titre
- Universality in two dimensions
- auteur
- Nachum Dershowitz, Gilles Dowek
- article
- Journal of Logic and Computation, 2013, ⟨10.1093/logcom/ext022⟩
- identifiant
- hal-00919604
- Accès au texte intégral et bibtex
-
- titre
- Causal graph dynamics
- auteur
- Pablo Arrighi, Gilles Dowek
- article
- Information and Computation, 2013, 223, pp.78-93. ⟨10.1016/j.ic.2012.10.019⟩
- identifiant
- hal-00944459
- Accès au bibtex
-
- titre
- Typing linear algebra: A biproduct-oriented approach
- auteur
- Hugo Daniel Macedo, José N. Oliveira
- article
- Science of Computer Programming, 2013, 78 (11), pp.2160-2191. ⟨10.1016/j.scico.2012.07.012⟩
- identifiant
- hal-00919866
- Accès au texte intégral et bibtex
-
- titre
- Lineal: A linear-algebraic lambda-calculus
- auteur
- Pablo Arrighi, Gilles Dowek
- article
- Logical Methods in Computer Science, 2013
- identifiant
- hal-00919625
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Semantic A-translation and Super-consistency entail Classical Cut Elimination
- auteur
- Lisa Allali, Olivier Hermant
- article
- LPAR 19 - 19th Conference on Logic for Programming, Artificial Intelligence, and Reasoning - 2013, Bernd Fischer, Geoff Sutcliffe, Dec 2013, Stellenbosch, South Africa. pp.407-422, ⟨10.1007/978-3-642-45221-5_28⟩
- identifiant
- hal-00923915
- Accès au texte intégral et bibtex
-
- titre
- Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo
- auteur
- David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
- article
- LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. pp.274-290, ⟨10.1007/978-3-642-45221-5_20⟩
- identifiant
- hal-00909784
- Accès au texte intégral et bibtex
-
- titre
- Polarizing Double Negation Translations
- auteur
- Mélanie Boudard, Olivier Hermant
- article
- LPAR, Dec 2013, Stellenbosch, South Africa. pp.182-197
- identifiant
- hal-00920224
- Accès au texte intégral et bibtex
-
- titre
- Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps
- auteur
- David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
- article
- IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa
- identifiant
- hal-00909688
- Accès au texte intégral et bibtex
-
- titre
- Towards explicit rewrite rules in the λΠ-calculus modulo
- auteur
- Ronan Saillard
- article
- IWIL - 10th International Workshop on the Implementation of Logics, Dec 2013, Stellenbosch, South Africa
- identifiant
- hal-00921340
- Accès au texte intégral et bibtex
-
- titre
- Detection of First Order Axiomatic Theories
- auteur
- Guillaume Burel, Simon Cruanes
- article
- FroCoS - 9th International Symposium on Frontiers of Combining Systems - 2013, Sep 2013, Nancy, France. pp.229-244, ⟨10.1007/978-3-642-40885-4_16⟩
- identifiant
- hal-00919759
- Accès au texte intégral et bibtex
-
- titre
- Mining Malware Specifications through Static Reachability Analysis
- auteur
- Hugo Daniel Macedo, Tayssir Touili
- article
- ESORICS 2013 - 18th European Symposium on Research in Computer Security, Sep 2013, Egham, United Kingdom. pp.517-535, ⟨10.1007/978-3-642-40203-6_29⟩
- identifiant
- hal-00919782
- Accès au texte intégral et bibtex
-
- titre
- The probability of non-confluent systems
- auteur
- Alejandro Díaz-Caro, Gilles Dowek
- article
- DCM - 9th International Workshop on Developments in Computational Models - 2013, Aug 2013, Buenos Aires, Argentina. pp.1-15, ⟨10.4204/EPTCS.144.1⟩
- identifiant
- hal-00919546
- Accès au texte intégral et bibtex
-
- titre
- Square root and division elimination in PVS
- auteur
- Pierre Neron
- article
- ITP - 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.457-462, ⟨10.1007/978-3-642-39634-2_33⟩
- identifiant
- hal-00924359
- Accès au texte intégral et bibtex
-
- titre
- Real numbers, chaos, and the principle of a bounded density of information
- auteur
- Gilles Dowek
- article
- CSR 2013 - 8th International Computer Science Symposium in Russia, Jun 2013, Ekaterinburg, Russia. pp.347-353, ⟨10.1007/978-3-642-38536-0_30⟩
- identifiant
- hal-00919543
- Accès au texte intégral et bibtex
-
- titre
- Programming Robots With Events
- auteur
- Truong Giang Le, Dmitriy Fedosov, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo
- article
- 4th International Embedded Systems Symposium (IESS), Jun 2013, Paderborn, Germany. pp.14-25, ⟨10.1007/978-3-642-38853-8_2⟩
- identifiant
- hal-00924489
- Accès au texte intégral et bibtex
-
- titre
- A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo
- auteur
- Guillaume Burel
- article
- PxTP - Third International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. pp.43-57
- identifiant
- hal-00921513
- Accès au texte intégral et bibtex
-
- titre
- Call-by-value non-determinism in a linear logic type discipline
- auteur
- Alejandro Díaz-Caro, Giulio Manzonetto, Michele Pagani
- article
- LFCS - Logical Foundations of Computer Science - 2013, Jan 2013, San Diego, CA, United States. pp.164-178, ⟨10.1007/978-3-642-35722-0_12⟩
- identifiant
- hal-00919463
- Accès au texte intégral et bibtex
-
- titre
- Using Event-Based Style for Developing M2M Applications
- auteur
- Truong Giang Le, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo
- article
- GPC - 8th International Conference on Grid and Pervasive Computing - 2013, 2013, Seoul, South Korea. pp.348-357, ⟨10.1007/978-3-642-38027-3_37⟩
- identifiant
- hal-00924491
- Accès au texte intégral et bibtex
-
Books
- titre
- Informatique et sciences du numérique : Édition spéciale Python
- auteur
- Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Claudio Cimellli, Albert Cohen, Christine Eisenbeis, Thierry Viéville, Benjamin Wack, Hugues Bersini, Guillaume Le Blanc
- article
- Eyrolles, pp.352, 2013, 978-2212136760
- identifiant
- hal-01262640
- Accès au bibtex
-
- titre
- Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python
- auteur
- Judicaël Courant, Marc de Falco, Stéphane Gonnord, Jean-Christophe Filliâtre, Sylvain Conchon, Gilles Dowek, Benjamin Wack
- article
- Eyrolles, pp.1-390, 2013, 978-2-212-13700-2
- identifiant
- hal-00880268
- Accès au bibtex
-
Poster communications
- titre
- Dedukti:un vérificateur de preuves universel
- auteur
- Ali Assaf, Raphaël Cauderlier, Ronan Saillard
- article
- Journées nationales GDR - GPL - CIEL - AFADL, Apr 2013, Nancy, France
- identifiant
- hal-01086609
- Accès au texte intégral et bibtex
-
- titre
- Elimination des racines et divisions pour du code embarqué
- auteur
- Pierre Neron
- article
- Journées du GDR-GPL, Apr 2013, Nancy, France
- identifiant
- hal-00924394
- Accès au texte intégral et bibtex
-
Reports
- titre
- Médiation Scientifique : une facette de nos métiers de la recherche
- auteur
- Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia, Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak, Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane, Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic, Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi, Muriel Droin, Nathalie Lacaux, Nicolas P. Rougier, Nicolas Roussel, Pascal Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas, Sophie de Quatrebarbes, Stéphane Laurent
- article
- [Interne] Inria. 2013, pp.34
- identifiant
- hal-00804915
- Accès au texte intégral et bibtex
-
Theses
- titre
- A Quest for Exactness: Program Transformation for Reliable Real Numbers
- auteur
- Pierre Neron
- article
- Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English. ⟨NNT : ⟩
- identifiant
- pastel-00960808
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- On the definition of the classical connectives and quantifiers
- auteur
- Gilles Dowek
- article
- 2013
- identifiant
- hal-00919437
- Accès au texte intégral et bibtex
-
- titre
- Informatics in the classification of sciences
- auteur
- Gilles Dowek
- article
- 2013
- identifiant
- hal-04051521
- Accès au texte intégral et bibtex
-
2012
Journal articles
- titre
- The Physical Church-Turing Thesis and the Principles of Quantum Theory
- auteur
- Pablo Arrighi, Gilles Dowek
- article
- International Journal of Foundations of Computer Science, 2012, 23 (5), pp.1131-1146. ⟨10.1142/S0129054112500153⟩
- identifiant
- hal-00944482
- Accès au bibtex
-
- titre
- A simple proof that super consistency implies cut elimination
- auteur
- Gilles Dowek, Olivier Hermant
- article
- Notre Dame Journal of Formal Logic, 2012, 53 (4), pp. 93-106. ⟨10.1215/00294527-1722692⟩
- identifiant
- hal-00793008
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- ML Dependency Analysis for Assessors
- auteur
- François Pessaux, Vincent Benayoun, Catherine Dubois, Philippe Ayrault
- article
- Software Engineering and Formal Methods (SEFM) 2012, Oct 2012, Thessaloniki, Greece. pp.278-292, ⟨10.1007/978-3-642-33826-7_19⟩
- identifiant
- hal-01203505
- Accès au texte intégral et bibtex
-
- titre
- Non determinism through type isomorphism
- auteur
- Alejandro Díaz-Caro, Gilles Dowek
- article
- LSFA - 7th Workshop on Logical and Semantic Frameworks with Applications - 2012, Sep 2012, Rio de Janeiro, Brazil. pp.137-144, ⟨10.4204/EPTCS.113.13⟩
- identifiant
- hal-00925001
- Accès au bibtex
-
- titre
- Causal Graph Dynamics
- auteur
- Pablo Arrighi, Gilles Dowek
- article
- ICALP 2012 - 39th International ColloquiumAutomata, Languages, and Programming, Jul 2012, Warwick, United Kingdom. pp.54-66, ⟨10.1007/978-3-642-31585-5_9⟩
- identifiant
- hal-00944492
- Accès au bibtex
-
- titre
- Tableaux Modulo Theories Using Superdeduction
- auteur
- Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
- article
- IJCAR 2012 - 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, UK, United Kingdom. pp.1 - 13, ⟨10.1007/978-3-642-31365-3_26⟩
- identifiant
- hal-01099338
- Accès au texte intégral et bibtex
-
Master thesis
- titre
- Traduction de HOL en Dedukti
- auteur
- Ali Assaf
- article
- Logique en informatique [cs.LO]. 2012
- identifiant
- hal-00919871
- Accès au texte intégral et bibtex
-
Books
- titre
- Informatique et Sciences du Numérique - Spécialité ISN en Terminale S
- auteur
- Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Claudio Cimellli, Albert Cohen, Christine Eisenbeis, Thierry Viéville, Benjamin Wack
- article
- Eyrolles, pp.303, 2012, 978-2-212-13543-5
- identifiant
- hal-00765220
- Accès au bibtex
-
- titre
- Informatique et sciences du numérique ― Spécialité ISN en terminale S, avec des exercices corrigés et des idées de projets
- auteur
- Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Claudio Cimelli, Albert Cohen, Christine Eisenbeis, Thierry Viéville, Benjamin Wack, Gérard Berry
- article
- Eyrolles, 2012
- identifiant
- hal-01257263
- Accès au bibtex
-
- titre
- Natural Computing
- auteur
- Olivier Bournez, Gilles Dowek
- article
- Springer, pp.1, 2012
- identifiant
- hal-00760732
- Accès au bibtex
-
Preprints, Working Papers, ...
- titre
- Causal graph dynamics
- auteur
- Pablo Arrighi, Gilles Dowek
- article
- 2012
- identifiant
- hal-00944505
- Accès au bibtex
-
- titre
- Algorithmes et modèles : l'histoire d'une convergence
- auteur
- Gilles Dowek
- article
- 2012
- identifiant
- hal-04061691
- Accès au texte intégral et bibtex
-
- titre
- A theory independent Curry-De Bruijn-Howard correspondence
- auteur
- Gilles Dowek
- article
- 2012
- identifiant
- hal-04070185
- Accès au texte intégral et bibtex
-
- titre
- Enseigner les sciences au XXIe siècle
- auteur
- Gilles Dowek
- article
- 2012
- identifiant
- hal-04048560
- Accès au texte intégral et bibtex
-
2011
Conference papers
- titre
- The physical Church-Turing thesis and the principles of quantum theory
- auteur
- Pablo Arrighi, Gilles Dowek
- article
- QIPC, 2011, Zurich, Switzerland. Local proceedings
- identifiant
- hal-00944544
- Accès au bibtex
-
Books
- titre
- Une introduction à la science informatique pour les enseignants de la discipline en lycée
- auteur
- Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Sylvie Boldo, Denis Bouhineau, Patrick Cegielski, Thomas Heide Clausen, Irène Guessarian, Stéphane Lopes, Laurent Mounier, Benjamin Nguyen, Franck Quessette, Anne Rasse, Brigitte Rozoy, Claude Timsit, Thierry Viéville, Jean-Marc Vincent
- article
- Gilles Dowek. CRDP Paris, pp.376, 2011, Repères pour agir (RPA disciplines & compétences), Christine Moulin, 978-2-86631-188-9
- identifiant
- hal-00765226
- Accès au bibtex
-
2010
Preprints, Working Papers, ...
- titre
- A second Galilean revolution?
- auteur
- Gilles Dowek
- article
- 2010
- identifiant
- hal-04048357
- Accès au texte intégral et bibtex
-
2008
Preprints, Working Papers, ...
- titre
- Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View
- auteur
- Gilles Dowek
- article
- 2008
- identifiant
- hal-04088449
- Accès au texte intégral et bibtex
-
2005
Preprints, Working Papers, ...
- titre
- A constructive proof of Skolem theorem for constructive logic
- auteur
- Gilles Dowek, Benjamin Werner
- article
- 2005
- identifiant
- hal-04099179
- Accès au texte intégral et bibtex
-
- titre
- What do we know when we know that a theory is consistent?
- auteur
- Gilles Dowek
- article
- 2005
- identifiant
- hal-04099146
- Accès au texte intégral et bibtex
-