Chargé de recherches CNRS, Loria, UMR 7503   Equipe TYPES, responsable Didier Galmiche

Informations générales

• Equipe TYPES, LORIA
  
• Clef GPG : test for GT PARANO
• Logiciels
  • STRIP, preuves et contre-modèles pour la logique intuitionniste
  • BOOLIN, preuves et contre-modèles pour la logique de Gödel-Dummett
  • BBI-Coq, preuve formelle en Coq de la complétude forte de Boolean BI
  • BI-Coq, preuve formelle en Coq de la complétude forte de BI
  • Kruskal-Coq, preuve inductive en Coq des théorèmes de Higman et de Kruskal
  • Lambda Calcul: implementation purement constructive avec des types dépendants et indices à la De Bruijn.
  • Decidability for Implicational Relevance Logic via a constructivized Kripke-Curry proof based on redundancy avoindance.
  • Semantic Cut-Elimination for ILL via relational phase semantics.
  • A library of formalised undecidable problems in Coq: inclu machines de Turing, problème de correspondance de Post, machine à piles binaires, machines de Minsky (à compteurs), logique du premier ordre, logique linéaire, équations Diophantiniennes dont la preuve d'insolvabilité du 10ième problème Hilbert, etc.

Domaines de recherche

• Logiques intermédiaires entre logique intuitionniste et logique classique.
• Logiques de ressources, logiques linéaires, logiques de séparation.
  
• Recherche de preuves et de contre-modèles, implantations efficaces

Publications

• Dominique Larchey-Wendling
  The Coq-Kruskal project, a user friendly Coq script adapting of Wim Veldman's approach to Kruskal's tree theorem,
  using Almost Full relations as defined inductively by Thierry Coquand. 2024.
  
  
• Dominique Larchey-Wendling
  Quasi Morphisms for Almost Full relations (artifact on GitHub)
  Presented at TYPES 2024 (slides, record of the talk).
  
  
• Dominique Larchey-Wendling and Jean-François Monin
  Proof pearl: faithful computation and extraction of µ-recursive algorithms in Coq (preprint)
  (Coq source code available on GitHub)
  Interactive Theorem Proving, ITP 2023.
  
  
• Dominik Kirst, Johannes Hostert, Andrej Dudenhefner, Yannick Forster, Marc Hermes, Mark Koch,
  Dominique Larchey-Wendling, Niklas Mück, Benjamin Peters, Gert Smolka and Dominik Wehr
  A Coq Library for Mechanised First-Order Logic (slides)
  The Coq Workshop 2022.
  
  
• Dominik Kirst and Dominique Larchey-Wendling
  Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
  (Coq source code available on GitHub)
  Logical Methods in Computer Science, 29 pages, June 14, 2022.
  
  
• Dominique Larchey-Wendling and Yannick Forster
  Hilbert's Tenth Problem in Coq (extended version)
  (Coq source code available on GitHub)
  Logical Methods in Computer Science, 41 pages, March 1, 2022.
  
  
• Dominique Larchey-Wendling and Jean-François Monin
  The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq (preprint)
  Chapter 8 (82 pages) (Coq source code available on GitHub)
  in Proof and Computation II: From Proof Theory and Univalent Mathematics to Program Extraction and Verification.
  Klaus Mainzer, Peter Schuster, Helmut Schwichtenberg (eds.), World Scientific Singapore, August 2021.
  
  
• Dominique Larchey-Wendling
  Extraction of recursive algorithms in Coq using the Braga method
  Invited talk (1h) at ASL Logic Colloqium 2020/21, July 24, 2021.
  
  
• Dominique Larchey-Wendling
  Synthetic Undecidability of MSELL via FRACTRAN mechanised in Coq
  (Coq source code available on GitHub)
  Formal Structures for Computation and Deduction FSCD 2021 (slides).
  
  
• Dominik Kirst and Dominique Larchey-Wendling
  Trakhtenbrot's Theorem in Coq (extended preprint here)
  (Coq source code available on GitHub)
  International Joint Conference on Automated Reasonning IJCAR 2020.
  
  
• Dominique Larchey-Wendling
  Constructive Decision via Redundancy-free Proof-Search (extended) (preprint here)
  (Coq source code available on GitHub)
  Journal of Automated Reasonning, 23 pages, 24 June 2020,
  Special issue: Selected Extended Papers from IJCAR 2018.
  
  
• Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Dominik Kirst, et al
  A Coq Library of Undecidable Problems (GitHub repository)
  The Sixth International Workshop on Coq for Programming Languages CoqPL 2020.
  
  
• Dominique Larchey-Wendling and Ralph Matthes
  Certification of Breadth-First Algorithms by Extraction (preprint here)
  (Coq source code available on GitHub)
  Mathematics of Program Construction MPC 2019.
  
  
• Dominique Larchey-Wendling
  Extraction of programs in Coq, invited course (3x1h)
  PC19, Autumn school "Proof and Computation", Sep 20-26, 2019.
  
  
• Dominique Larchey-Wendling and Yannick Forster
  Hilbert's Tenth Problem in Coq (preprint here)
  (Coq source code available on GitHub)
  Formal Structures for Computation and Deduction FSCD 2019 (slides).
  
  
• Yannick Forster and Dominique Larchey-Wendling
  Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines (preprint here)
  (Coq source code available on GitHub)
  Certified Programs and Proofs CPP 2019.
  
  
• Dominique Larchey-Wendling and Jean-François Monin
  Simulating Induction-Recursion for Partial Algorithms
  (Coq source code available on GitHub)
  Presented at TYPES 2018.
  
  
• Dominique Larchey-Wendling
  Constructive Decision via Redundancy-free Proof-Search (preprint here)
  (Coq source code available on GitHub)
  International Joint Conference on Automated Reasonning IJCAR 2018.
  
  
• Dominique Larchey-Wendling
  Proof Pearl: Constructive Extraction of Cycle Finding Algorithms (preprint here)
  (Coq source code available on GitHub)
  Interactive Theorem Proving, ITP 2018.
  
  
• Dominique Larchey-Wendling
  Typing Total Recursive Functions in Coq (preprint here)
  (Coq source code available on GitHub)
  Interactive Theorem Proving, ITP 2017 (slides).
  
  
• Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling and Daniel Méry
  Separation Logic with One Quantified Variable (extended and complete version) (preprint here)
  Theory of Computing Systems, 91 pages, May 2017.
  
  
• Dominique Larchey-Wendling and Didier Galmiche
  Looking at Separation Algebras with Boolean BI-eyes (full version)
  Theoretical Computer Science, TCS 2014.
  
  
• Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling and Daniel Méry
  Separation Logic with One Quantified Variable
  Computer Science Russia, CSR 2014.
  
  
• Dominique Larchey-Wendling
  The formal strong completeness of partial monoidal Boolean BI (preprint here)
  Journal of Logic and Computation, 36 pages, June 2014.
  
  
• Dominique Larchey-Wendling and Didier Galmiche
  Non-deterministic Phase Semantics and the Undecidability of Boolean BI
  ACM Transactions on Computational Logic (TOCL), vol 14(1), 41 pages, 2013.
  
  
• Dominique Larchey-Wendling and Didier Galmiche
  The Undecidability of Boolean BI through Phase Semantics (full version)
  Logic in Computer Science, LICS 2010.
  
  
• Dominique Larchey-Wendling
  An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics
  Mathematical Foundations of Programming Semantics, MFPS 2010 (slides).
  Electronic Notes in Theoretical Computer Science, vol 265, pp 369-387, 2010.
  
  
• Didier Galmiche, Dominique Larchey-Wendling and Joseph Vidal-Rosset
  Some Remarks on Relations between Proofs and Games
  In Festschrift for Gerhard Heinzmann, College Publications, 2010.
  
  
• Dominique Larchey-Wendling and Didier Galmiche
  Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
  Mathematical Structures in Computer Science, vol 19(3), pp 435-500, 2009
  
  
• Dominique Larchey-Wendling
  Graph based decision for Gödel-Dummett logics
  Journal of Automated Reasoning, vol 38, pp 201-225, 2007.
  
  
• Didier Galmiche and Dominique Larchey-Wendling
  Expressivity properties of Boolean BI through relational models
  Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006.
  
  
• Dominique Larchey-Wendling
  Bounding resource consumption with Gödel-Dummett logics
  12th International conference, LPAR 2005.
  
  
• Dominique Larchey-Wendling
  Gödel-Dummett counter-models through matrix computation
  Electronic Notes in Theoretical Computer Science, vol 125, num 3, 2005.
  
  
• Dominique Larchey-Wendling
  Counter-model search in Gödel-Dummett logics
  International Joint Conference on Automated Reasoning, IJCAR 2004.
  
  
• Dominique Larchey-Wendling
  Combining proof-search and counter-model construction for deciding Gödel-Dummett logic
  International Conference on Automated Deduction, CADE 2002.
  
  
• Dominique Larchey-Wendling, Daniel Mery and Didier Galmiche
  STRIP: Structural Sharing for Efficient Proof-search
  International Joint Conference on Automated Reasoning, IJCAR 2001.
  
  
• Didier Galmiche and Dominique Larchey-Wendling
  Quantales as completions of ordered monoids: revised semantics for Intuitionistic Linear Logic
  Electronic Notes in Theoretical Computer Science, vol 35, 2000.
  
  
• Didier Galmiche and Dominique Larchey-Wendling
  Structural sharing and efficient proof-search in propositional intuitionistic logic
  Asian Computing Science Conference, ASIAN'99.
  
  
• Didier Galmiche and Dominique Larchey-Wendling
  Provability in Intuitionistic Linear Logic from a New Interpretation on Petri nets (extended abstract)
  Electronic Notes in Theoretical Computer Science, vol 17, 1998.
  
  
• Didier Galmiche and Dominique Larchey-Wendling
  Formulae-as-Resources Management for an Intuitionistic Theorem Prover
  5th Workshop on Logic, Language, Information and Computation, WoLLIC'98.
  
  

Editeur

• Didier Galmiche and Dominique Larchey-Wendling
  Automated Reasoning with Analytic Tableaux and Related Methods, LNAI 8123
  22th International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013 Proceedings
  
  
• Jack Copeland, Didier Galmiche, Dominique Larchey-Wendling and Jospeh Vidal-Rosset
  Philosophia Scientiae, "Alan Turing", volume 16, cahier 3, 2012.
  Edition Kimé, Paris, ISBN 978-2-84174-603-3
  
  

Exposés à des Workshops

• Dominique Larchey-Wendling and Jean-François Monin
  The Braga method and the extraction of complex recursive algorithms (slides) (Coq code)
  GT Coq, Bordeaux, April 2023.
  
  
• Dominique Larchey-Wendling et al.
  Coq Library of Undecidability Proofs (slides)
  Journées GT Calculabilités, Nancy, October 2022.
  
  
• Yannick Forster and Dominique Larchey-Wendling
  A constructive Coq library for the mechanization of undecidability (slides)
  MLA 2019, Nancy, March 2019.
  
  
• Dominique Larchey-Wendling
  Mechanizing Cut-Elimination in Coq via Relational Phase Semantics (slides)
  (Coq source code available on GitHub).
  Preuves de logique linéaire sur machine, ENS-Lyon, December 2018.
  
  
• Yannick Forster and Dominique Larchey-Wendling
  Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
  LOLA 2018, Oxford, July 2018.
  
  
• Dominique Larchey-Wendling and Jean-François Monin
  Simulating Induction-Recursion for Partial Algorithms
  Invited talk at the Programming Systems Lab, Saarland University, March 2018.
  
  
• Dominique Larchey-Wendling
  Mechanising Undecidability results in Coq: Elementary Linear Logic and Boolean BI (slides).
  Second SYSMICS Workshop, Vienna, February 2018.
  
  
• Dominique Larchey-Wendling
  The Computational Content of the Constructive Kruskal Tree Theorem
  Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2017), Nancy, June 2017.
  
  
• Dominique Larchey-Wendling
  Kruskal's tree theorem in Type Theory (slides)
  Workshop on Foundations for the practical formalization of mathematics (FPFM), April 2017.
  
  
• Dominique Larchey-Wendling
  Kruskal's tree theorem in Type Theory (slides)
  Mathematics for Computation (M4C), Allemagne, Mai 2016.
  
  
• Dominique Larchey-Wendling
  An axiom free Coq proof of Kruskal's tree theorem (slides)
  Well-Quasiorders in Computer Science - Dagstuhl Seminar 16031, Janurary 2016.
  
  
• Dominique Larchey-Wendling
  The subformula property in intuitionistic sequents proof search (slides)
  Classical Logic vs. Intuitionistic Logic, Nancy, Mai 2012
  
  
• Dominique Larchey-Wendling
  Phase Semantics and the Undecidability of Boolean BI (slides)
  Geocal-Lac, Nancy, Mai 2011.
  
  
• Dominique Larchey-Wendling
  Labelled Tableaux for Proofs and Models in BI logics (slides)
  Automated Deduction Day, Nancy, Juillet 2009.
  
  
• Dominique Larchey-Wendling
  Kripke Models of Boolean BI and Invertible resources (abstract, slides)
  Domains IX Workshop 08, Brighton, GB, 22-24 septembre 2008.
  
  
• Didier Galmiche, Dominique Larchey and Yakoub Salhi
  Hypersequents and Countermodels in Gödel-Dummett Logics
  CADE'07 - Workshop on Disproving: non-theorems, non-validity, non-provability, Brême, Allemagne, 16 juillet 2007.
  
  
• Dominique Larchey-Wendling
  Relational semantics and finite models of separation logics
  CMF'2007 - Modèles de calcul, Modèles finis et Complexité, Nancy, France, 21-22 mai 2007.
  
  
• Dominique Larchey-Wendling
  Resources, process calculi and Gödel logic
  Workshop on Logic Nancy-Saarbrücken - Proofs and Programs, Nancy, France, 13-14 octobre 2005.
  
  
• Dominique Larchey-Wendling
  Gödel-Dummett counter-models through matrix computation
  IJCAR 2004 - Workshop on Disproving: non-theorems, non-validity, non-provability Cork, Irlande, 5 juillet 2004.
  
  
• Dominique Larchey-Wendling
  Combining proof search and linear counter-model construction
  First APPSEM-II Workshop, Nottingham, Royaume Uni, 26-28 mars 2003.
  
  
• Dominique Larchey-Wendling
  Refutations as finite resource counter-models
  Workshop on Semantic Foundations of Proof-search, Dagstuhl, Wadern, Allemagne, 1-6 avril 2001.
  
  
• Dominique Larchey-Wendling and Didier Galmiche
  From ordered monoids to quantales and Petri nets: completeness results revisited in Intuitionistic Linear Logic
  Workshop on Domains IV, Rolandseck, Allemagne, 2-4 octobre 1998.
  
  
• Dominique Larchey-Wendling and Didier Galmiche
  Provability in Intuitionistic Linear Logic from a new interpretation on Petri nets
  CADE-15 Workshop on Proof Search in Type-Theoretic Languages, Lindau, Allemagne, 5 juillet 1998.
  
  

Rapports techniques

• Dominique Larchey-Wendling
  Preuves, réfutations et contre-modèles dans des logiques intuitionnistes
  Thèse de l'université Henri Poincaré, Nancy I, 2000.
  
  
• Dominique Larchey-Wendling and Didier Galmiche
  Resource models and proof-search in Intuitionistic Linear Logic
  Université Henri Poincaré, 2000.
  
  

Adresse de travail

Dominique Larchey-Wendling
CNRS, Bâtiment LORIA, BP 239
54506 Vandoeuvre-lès-Nancy
France

email: larchey at loria.fr
gpg pubkey: professional and test (GT PARANO)
Téléphone: +33 (0) 3 54 95 85 14
Fax: +33 (0) 3 83 41 30 79