default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDDominique Larchey-Wendling
Person information
- affiliation: University of Lorraine, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
[c22]Dominique Larchey-Wendling, Jean-François Monin:
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. ITP 2023: 21:1-21:17- [i4]Tim S. Lyon, Agata Ciabattoni, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry, Nicola Olivetti, Revantha Ramanayake:
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations. CoRR abs/2312.03426 (2023) - 2022
- [j8]Dominique Larchey-Wendling, Yannick Forster:
Hilbert's Tenth Problem in Coq (Extended Version). Log. Methods Comput. Sci. 18(1) (2022) - [j7]Dominik Kirst
, Dominique Larchey-Wendling:
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens. Log. Methods Comput. Sci. 18(2) (2022) - 2021
- [c21]Dominique Larchey-Wendling:
Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq. FSCD 2021: 18:1-18:20 - [i3]Dominik Kirst, Dominique Larchey-Wendling:
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens. CoRR abs/2104.14445 (2021) - 2020
- [j6]Dominique Larchey-Wendling:
Constructive Decision via Redundancy-Free Proof-Search. J. Autom. Reason. 64(7): 1197-1219 (2020) - [c20]Dominik Kirst, Dominique Larchey-Wendling:
Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory. IJCAR (2) 2020: 79-96 - [i2]Dominique Larchey-Wendling, Yannick Forster:
Hilbert's Tenth Problem in Coq. CoRR abs/2003.04604 (2020) - [i1]Dominik Kirst, Dominique Larchey-Wendling:
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory. CoRR abs/2004.07390 (2020)
2010 – 2019
- 2019
- [c19]Yannick Forster, Dominique Larchey-Wendling:
Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. CPP 2019: 104-117 - [c18]Dominique Larchey-Wendling, Ralph Matthes:
Certification of Breadth-First Algorithms by Extraction. MPC 2019: 45-75 - [c17]Dominique Larchey-Wendling, Yannick Forster:
Hilbert's Tenth Problem in Coq. FSCD 2019: 27:1-27:20 - 2018
- [c16]Dominique Larchey-Wendling:
Constructive Decision via Redundancy-Free Proof-Search. IJCAR 2018: 422-438 - [c15]Dominique Larchey-Wendling:
Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. ITP 2018: 370-387 - 2017
- [j5]Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry:
Separation Logic with One Quantified Variable. Theory Comput. Syst. 61(2): 371-461 (2017) - [c14]Dominique Larchey-Wendling:
Typing Total Recursive Functions in Coq. ITP 2017: 371-388 - 2016
- [j4]Dominique Larchey-Wendling:
The formal strong completeness of partial monoidal Boolean BI. J. Log. Comput. 26(2): 605-640 (2016) - 2014
- [c13]Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry:
Separation Logic with One Quantified Variable. CSR 2014: 125-138 - [c12]Dominique Larchey-Wendling, Didier Galmiche:
Looking at Separation Algebras with Boolean BI-eyes. IFIP TCS 2014: 326-340 - 2013
- [j3]Dominique Larchey-Wendling, Didier Galmiche:
Nondeterministic Phase Semantics and the Undecidability of Boolean BI. ACM Trans. Comput. Log. 14(1): 6:1-6:41 (2013) - [e1]Didier Galmiche, Dominique Larchey-Wendling:
Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013. Proceedings. Lecture Notes in Computer Science 8123, Springer 2013, ISBN 978-3-642-40536-5 [contents] - 2010
- [c11]Dominique Larchey-Wendling, Didier Galmiche:
The Undecidability of Boolean BI through Phase Semantics. LICS 2010: 140-149 - [c10]Dominique Larchey-Wendling:
An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics. MFPS 2010: 369-387
2000 – 2009
- 2009
- [j2]Dominique Larchey-Wendling, Didier Galmiche:
Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding. Math. Struct. Comput. Sci. 19(3): 435-500 (2009) - 2007
- [j1]Dominique Larchey-Wendling:
Graph-based Decision for Gödel-Dummett Logics. J. Autom. Reason. 38(1-3): 201-225 (2007) - 2006
- [c9]Didier Galmiche, Dominique Larchey-Wendling:
Expressivity Properties of Boolean. FSTTCS 2006: 357-368 - 2005
- [c8]Dominique Larchey-Wendling:
Bounding Resource Consumption with Gödel-Dummett Logics. LPAR 2005: 682-696 - 2004
- [c7]Dominique Larchey-Wendling:
Counter-Model Search in Gödel-Dummett Logics. IJCAR 2004: 274-288 - [c6]Dominique Larchey-Wendling:
Gödel-Dummett Counter-models through Matrix Computation. D/PDPAR@IJCAR 2004: 137-148 - 2002
- [c5]Dominique Larchey-Wendling:
Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic. CADE 2002: 94-110 - 2001
- [c4]Dominique Larchey-Wendling, Daniel Méry, Didier Galmiche:
STRIP: Structural Sharing for Efficient Proof-Search. IJCAR 2001: 696-700 - 2000
- [b1]Dominique Larchey-Wendling:
Preuves, réfutations et contre-modèles dans des logiques intuitionnistes. Henri Poincaré University, Nancy, France, 2000
1990 – 1999
- 1999
- [c3]Didier Galmiche, Dominique Larchey-Wendling:
Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic. ASIAN 1999: 101-112 - 1998
- [c2]Dominique Larchey-Wendling, Didier Galmiche:
Provability in Intuitionistic Linear Logic from a New Interpretation on Petri nets. Proof Search in Type-Theoretic Languages@CADE 1998: 1-18 - [c1]Dominique Larchey-Wendling, Didier Galmiche:
Quantales as completions of ordered monoids - Revised semantics for Intuitionistic Linear Logic. Workshop on Domains 1998: 94-108
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:15 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
