| Expressivity properties of Boolean BI through relational models D Galmiche, D Larchey-Wendling International Conference on Foundations of Software Technology and …, 2006 | 72 | 2006 |
| The undecidability of boolean BI through phase semantics D Larchey-Wendling, D Galmiche 2010 25th Annual IEEE Symposium on Logic in Computer Science, 140-149, 2010 | 68 | 2010 |
| Hilbert's Tenth Problem in Coq (Extended Version) D Larchey-Wendling, Y Forster Logical Methods in Computer Science 18, 2022 | 58 | 2022 |
| Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding D Larchey-Wendling, D Galmiche Mathematical Structures in Computer Science 19 (3), 435-500, 2009 | 50 | 2009 |
| A Coq library of undecidable problems Y Forster, D Larchey-Wendling, A Dudenhefner, E Heiter, D Kirst, F Kunze, ... CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, 2020 | 48 | 2020 |
| Separation logic with one quantified variable S Demri, D Galmiche, D Larchey-Wendling, D Méry Theory of Computing Systems 61 (2), 371-461, 2017 | 42 | 2017 |
| Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines Y Forster, D Larchey-Wendling Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019 | 33 | 2019 |
| Alan Turing J Copeland, D Galmiche, D Larchey-Wendling, J Vidal-Rosset | 32 | 2012 |
| The formal strong completeness of partial monoidal Boolean BI D Larchey-Wendling Journal of Logic and Computation 26 (2), 605-640, 2016 | 31 | 2016 |
| Nondeterministic phase semantics and the undecidability of Boolean BI D Larchey-Wendling, D Galmiche ACM Transactions on Computational Logic (TOCL) 14 (1), 1-41, 2013 | 30 | 2013 |
| Trakhtenbrot’s theorem in Coq: a constructive approach to finite model theory D Kirst, D Larchey-Wendling Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris …, 2020 | 24 | 2020 |
| STRIP: Structural sharing for efficient proof-search D Larchey-Wendling, D Méry, D Galmiche Automated Reasoning: First International Joint Conference, IJCAR 2001 Siena …, 2001 | 21 | 2001 |
| Counter-model search in Gödel-Dummett logics D Larchey-Wendling Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork …, 2004 | 19 | 2004 |
| Combining proof-search and counter-model construction for deciding Gödel-Dummett logic D Larchey-Wendling Automated Deduction—CADE-18: 18th International Conference on Automated …, 2002 | 17 | 2002 |
| Structural sharing and efficient proof-search in propositional intuitionistic logic D Galmiche, D Larchey-Wendling Annual Asian Computing Science Conference, 101-112, 1999 | 17 | 1999 |
| Typing total recursive functions in Coq D Larchey-Wendling Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017 | 16 | 2017 |
| Graph-based decision for Gödel-Dummett logics D Larchey-Wendling Journal of Automated Reasoning 38, 201-225, 2007 | 15 | 2007 |
| High intensity ion beams prospects for accelerators with Phoenix 28 GHz T Thuillier, JL Bouly, JC Curdy, E Froidefond, T Lamy, C Peaucelle, ... EPAC 2002 European Particle Accelerator Conference 8, 1744-1746, 2002 | 15* | 2002 |
| A Coq library for mechanised first-order logic D Kirst, J Hostert, A Dudenhefner, Y Forster, M Hermes, M Koch, ... The Coq Workshop 2022, 2022 | 13 | 2022 |
| Looking at separation algebras with Boolean BI-eyes D Larchey-Wendling, D Galmiche IFIP International Conference on Theoretical Computer Science, 326-340, 2014 | 13 | 2014 |