Dominique Larchey-Wendling

38 papers A* 1A 4B 11Misc 1Journal 12Unranked 8
YearRankTypeTitle / Venue / Authors
2026 B conf
Bar Inductive Predicates for Constructive Algebra in Rocq.
CPP
Dominique Larchey-Wendling
2024 — conf
Constructive Substitutes for Kőnig's Lemma.
TYPES
Dominique Larchey-Wendling
2023 J jnl
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations.
CoRR
Tim S. Lyon, Agata Ciabattoni, Didier Galmiche, Marianna Girlando, Dominique Larchey-Wendling, Daniel Méry, Nicola Olivetti, Revantha Ramanayake
2023 B conf
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq.
ITP
Dominique Larchey-Wendling, Jean-François Monin
2022 J jnl
Hilbert's Tenth Problem in Coq (Extended Version).
Log. Methods Comput. Sci.
Dominique Larchey-Wendling, Yannick Forster
2022 J jnl
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens.
Log. Methods Comput. Sci.
Dominik Kirst, Dominique Larchey-Wendling
2021 B conf
Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq.
FSCD
Dominique Larchey-Wendling
2021 J jnl
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens.
CoRR
Dominik Kirst, Dominique Larchey-Wendling
2020 J jnl
Constructive Decision via Redundancy-Free Proof-Search.
J. Autom. Reason.
Dominique Larchey-Wendling
2020 J jnl
Hilbert's Tenth Problem in Coq.
CoRR
Dominique Larchey-Wendling, Yannick Forster
2020 — conf
Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory.
IJCAR (2)
Dominik Kirst, Dominique Larchey-Wendling
2020 J jnl
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory.
CoRR
Dominik Kirst, Dominique Larchey-Wendling
2019 B conf
Certification of Breadth-First Algorithms by Extraction.
MPC
Dominique Larchey-Wendling, Ralph Matthes
2019 B conf
Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines.
CPP
Yannick Forster, Dominique Larchey-Wendling
2019 B conf
Hilbert's Tenth Problem in Coq.
FSCD
Dominique Larchey-Wendling, Yannick Forster
2018 A conf
Constructive Decision via Redundancy-Free Proof-Search.
IJCAR
Dominique Larchey-Wendling
2018 B conf
Proof Pearl: Constructive Extraction of Cycle Finding Algorithms.
ITP
Dominique Larchey-Wendling
2017 J jnl
Separation Logic with One Quantified Variable.
Theory Comput. Syst.
Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry
2017 B conf
Typing Total Recursive Functions in Coq.
ITP
Dominique Larchey-Wendling
2016 J jnl
The formal strong completeness of partial monoidal Boolean BI.
J. Log. Comput.
Dominique Larchey-Wendling
2014 — conf
Looking at Separation Algebras with Boolean BI-eyes.
IFIP TCS
Dominique Larchey-Wendling, Didier Galmiche
2014 Misc conf
Separation Logic with One Quantified Variable.
CSR
Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry
2013 B ed.
Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013. Proceedings
TABLEAUX
Didier Galmiche, Dominique Larchey-Wendling
2013 J jnl
Nondeterministic Phase Semantics and the Undecidability of Boolean BI.
ACM Trans. Comput. Log.
Dominique Larchey-Wendling, Didier Galmiche
2010 B conf
An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics.
MFPS
Dominique Larchey-Wendling
2010 A* conf
The Undecidability of Boolean BI through Phase Semantics.
LICS
Dominique Larchey-Wendling, Didier Galmiche
2009 J jnl
Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding.
Math. Struct. Comput. Sci.
Dominique Larchey-Wendling, Didier Galmiche
2007 J jnl
Graph-based Decision for Gödel-Dummett Logics.
J. Autom. Reason.
Dominique Larchey-Wendling
2006 — conf
Expressivity Properties of Boolean.
FSTTCS
Didier Galmiche, Dominique Larchey-Wendling
2005 B conf
Bounding Resource Consumption with Gödel-Dummett Logics.
LPAR
Dominique Larchey-Wendling
2004 A conf
Counter-Model Search in Gödel-Dummett Logics.
IJCAR
Dominique Larchey-Wendling
2004 — conf
Gödel-Dummett Counter-models through Matrix Computation.
D/PDPAR@IJCAR
Dominique Larchey-Wendling
2002 A conf
Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic.
CADE
Dominique Larchey-Wendling
2001 A conf
STRIP: Structural Sharing for Efficient Proof-Search.
IJCAR
Dominique Larchey-Wendling, Daniel Méry, Didier Galmiche
2000 — —
Preuves, réfutations et contre-modèles dans des logiques intuitionnistes.
Dominique Larchey-Wendling
1999 — conf
Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic.
ASIAN
Didier Galmiche, Dominique Larchey-Wendling
1998 — conf
Provability in Intuitionistic Linear Logic from a New Interpretation on Petri nets.
Proof Search in Type-Theoretic Languages@CADE
Dominique Larchey-Wendling, Didier Galmiche
1998 — conf
Quantales as completions of ordered monoids - Revised semantics for Intuitionistic Linear Logic.
Workshop on Domains
Dominique Larchey-Wendling, Didier Galmiche