Didier GALMICHE
LORIA UMR 7503
TYPES Group: Logic, Proof Theory and Programming

JOURNAL, CONFERENCE, WORKSHOP PAPERS

Beth Semantics and Labelled Deduction for Intuitionistic
Sentential Calculus with Identity
D. Galmiche and M. Gawek and D. Mery
6th International Conference on Formal Structures for Computation
and Deduction, FSCD 2021
Buenos Aires, Argentina, Juky 2021
A preprint is available here: .pdf

An Epistemic Separation Logic with Action Models
H. van Ditmarsch and D. Galmiche and M Gawek
9th Indian Conference on Logic and its Applications, ICLA 2021,
Chennai, India, March 2021.
A preprint is available here: .pdf

Labelled Cyclic Proofs for Separation Logic
D. Galmiche and D. Mery
Journal of Logic and Computation, 31(3):892-922, 2021.
https://doi.org/10.1093/logcom/exab017
A preprint is available here: .pdf

Relating Labelled and Label-free Bunched Calculi in BI logic
D. Galmiche and M. Marti and D. Mery
In 28th Int. Conference on Automated Reasoning with Analytic Tableaux
and Related Methods, TABLEAUX 2019,
LNAI 11714, pages 130-146, London, UK, September 2019.
A preprint is available here: .pdf

A Substructural Epistemic Resource Logic: theory
and modelling applications
D. Galmiche and P. Kimmel and D. Pym
Journal of Logic and Computation, 29(8): 1251-1287, 2019.
A preprint is available here: .pdf

A Public Announcement Separation Logic
J-R. Courtault and H. van Ditmarsch and D. Galmiche
Mathematical Structures in Computer Science, 29(6):828-871, 2019.
A preprint is available here: .pdf

Proof Translations in BI Logic - extended abstract
D. Galmiche and M. Marti and D. Mery
1st Int. Workshop on External and Internal Calculi for
Non-Classical Logics, EICNCL 2018
Oxford, UK, July 2018
A preprint is available here: .pdf

Labelled Connection-based Proof Search for Multiplicative
Intuitionistic Linear Logic
D. Galmiche and D. Mery
3rd Int. Workshop on Automated Reasoning in Quantified
Non-Classical Logics, ARQNL 2018
Oxford, UK, July 2018
A preprint is available here: .pdf

Labelled Cyclic Proofs for Separation Logic
D. Galmiche and D. Mery
1st Int. Workshop on Automated Deduction for Separation Logic, ADSL 2018
Oxford, UK, July 2018
A preprint is available here: .pdf

A Modal Separation Logic for Resource Dynamics
J-R. Courtault and D. Galmiche
Journal of Logic and Computation, 28(4): 733-778, 2018.
A preprint is available here: .pdf

Tree-sequent calculi and decision procedures for intuitionistic modal logics
D. Galmiche and Y. Salhi
Journal of Logic and Computation, 28(5): 967-989, 2018.
A preprint is available here: .pdf

Separation Logic with One Quantified Variable
S. Demri and D. Galmiche and D. Larchey-Wendling and D. Mery
Theory of Computing Systems, (ToCS), 61(2):371-461, 2017.
A preprint is available here: .pdf

A Substructural Epistemic Resource Logic
D. Galmiche and P. Kimmel and D. Pym
Seventh Indian Conference on Logic and its Applications, ICLA 2017,
LNCS 10119, pages 77-91
Kanpur, India, January 2017
A preprint is available here: .pdf

A logic of Separating Modalities
J-R. Courtault and D. Galmiche and D. Pym
Theoretical Computer Science, 637:30-58, 2016
A preprint is available here: .pdf

About Intuitionistic Public Announcement Logic
Ph. Balbiani and D. Galmiche
Int. Conference on Advances in Modal Logic, AiML 2016, pp97-116
Budapest, Hungary, August 2016
A preprint is available here: .pdf

An Epistemic Separation Logic
J-R. Courtault and H. van Ditmarsch and D. Galmiche
Int. Workshop on Logic, Language, Information, and Computation, WoLLIC 2015
Bloomington, IN, USA, July 2015.
A preprint is available here: .pdf

Looking at Separation Algebras with Boolean BI-eyes
D. Larchey-Wendling and D. Galmiche
Int. Conference on Theoretical Computer Science, TCS 2014
Rome, Italy, September 2014
A preprint is available here: .pdf

A sequent calculus with labels for PAL
Ph. Balbiani and V. Demange and D. Galmiche
Int. Conference on Advances in Modal Logic 2014, AiML 2014
Groningen, Netherlands, August 2014
A preprint is available here: .pdf

Separation Logic with One Quantified Variable
S. Demri and D. Galmiche and D. Larchey-Wendling and D. Mery
Int. Computer Science Symposium in Russia, CSR 2014
Moscow, Russia, June 2014
A preprint is available here: .pdf

A Connection-based Characterization of Bi-intuitionistic Validity
D. Galmiche and D. Mery
Journal of Automated Reasoning, vol. 51, 2013
A preprint is available here: .pdf

Non-deterministic Phase Semantics and the Undecidability of Boolean BI
D. Larchey-Wendling and D. Galmiche
ACM Transactions on Computational Logic, vol. 14, 2013
A preprint is available here: .pdf

An Interactive Prover for Bi-intuitionistic Logic
J-R. Courtault and D. Galmiche and D. Mery
Int. Workshop on the Implementation of Logics, IWIL 2013
Stellenbosch, South Africa, December 2013
A preprint is available here: .pdf

A modal extension of Boolean BI for resource transformations
J-R. Courtault and D. Galmiche
Int. Workshop on Logics for Resources, Processes and Programs, LRPP 2013
Nancy, France, September 2013
A preprint is available here: .pdf

A Modal BI Logic for Dynamic Resource Properties
J-R. Courtault and D. Galmiche
Int. Symposium on Logical Foundations of Computer Science, LFCS 2013,
San Diego, CA, USA, January 2013
A preprint is available here: .pdf

A Connection-based Characterization of Bi-intuitionistic Validity
D. Galmiche and D. Mery
Int. Conference on Automated Deduction, CADE-23
Wroclaw, Poland, July 2011
A preprint is available here: .pdf

Sequent Calculi and Decidability for Intuitionistic Hybrid Logic
D. Galmiche and Y. Salhi
Journal of Information and Computation, vol. 209, n. 12, pp 1447-1463, 2011
A preprint is available here: .pdf

Some Remarks on Relations between Proofs and Games
D. Galmiche and D. Larchey-Wendling and J. Vidal-Rosset
Construction - Festschrift for Gerhard Heinzmann
editors P.E. Bour, M. Rebushi, L. Rollet, pp 397-410, College Publications, 2010
A preprint is available here: .pdf

Label-free Natural Deduction Systems for Intuitionistic and Classical Modal Logics
D. Galmiche and Y. Salhi
Journal of Applied Non Classical Logics, vol. 20, n. 4, pp 373-421, 2010
A preprint is available here: .pdf

A Family of Goedel Hybrid Logics
D. Galmiche and Y. Salhi
Journal of Applied Logic, vol. 8, pp 371-385, 2010
A preprint is available here: .pdf

The Undecidability of Boolean BI through Phase Semantics
D. Larchey-Wendling and D. Galmiche
25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010
Edinburgh, Scotland, U.K., July 2010
A preprint is available here: .pdf

Label-free Proof Systems for Intuitionistic Modal Logic IS5
D. Galmiche and Y. Salhi
Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-16
Dakar, Senegal, April 2010
A preprint is available here: .pdf

Tableaux and Resource Graphs for Separation Logic
D. Galmiche and D. Mery
Journal of Logic and Computation, vol. 20, n. 1, pp 189-231, 2010.
A preprint is available here: .ps - .pdf

Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
D. Larchey-Wendling and D. Galmiche
Mathematical Structures in Computer Science, vol. 19, pp 435 - 500, 2009
A preprint is available here: .pdf

Labelled Calculi for Lukasiewicz Logics
D. Galmiche and Y. Salhi
Int. Workshop on Logic, Language, Information and Computation, WoLLIC'08
Edimburg, July 2008
A preprint is available here: .ps - .pdf

Calculi for an Intuitionistic Hybrid Modal Logic
D. Galmiche and Y. Salhi
Int. Workshop on Intuitionistic Modal Logic and Applications, IMLA'08
CMU, Pittsburg, June 2008
A preprint is available here: .ps - .pdf

Models and Separation Logics for Resource Trees
N. Biri and D. Galmiche
Journal of Logic and Computation, 17:4, pp 687-726, 2007
A preprint is available here: .ps - .pdf

Provability and Countermodels in Goedel-Dummett Logics
D. Galmiche and D. Larchey-Wendling and Y. Salhi
Int. Workshop on Disproving, Non-theorems, Non-validity, Non-Prouvability, DISPROVING'07,
Bremen, Germany, July 2007.
A preprint is available here: .ps - .pdf

Connection-based proof search in intuitionistic logic from transitive closure of constraints
D. Galmiche and D. Mery
Int. Workshop on Automated Deduction: Decidability, Complexity, Tractability, ADDCT'07
Bremen, Germany, July 2007.
A preprint is available here: .ps - .pdf

Expressivity properties of Boolean BI through Relational Models
D. Galmiche and D. Larchey-Wendling
26th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006
Kolkata, India, December 2006.
A preprint is available here: .ps - .pdf

Labelled Structures and Provability in Resource Logics
E. Dumoulin and D. Galmiche
ICALP Workshop on Structures and Deduction, SD'05
Lisbon, Portugal, July 2005.
A preprint is available here: .ps - .pdf

Resource Graphs and Countermodels in Resource Logics
D. Galmiche and D. Mery
Electronic Notes in Theoretical Computer Science 125 (2005)
A preprint is available here: .pdf

Semantics of BI and Resource Tableaux.
D. Galmiche and D. Mery and D. Pym
Mathematical Structures in Computer Science, vol. 15, n. 6, pp 1033-1088, 2005
A preprint is available here: .ps - .pdf

Characterizing Provability in BI's Pointer Logic through Resource Graphs
D. Galmiche and D. Mery
Int. Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2005
Montego Bay, Jamaica, December 2005.
A preprint is available here: .ps - .pdf

Resource Graphs and Countermodels in Resource Logics
D. Galmiche and D. Mery
Workshop on Disproving: Non-Theorems, Non-validity, Non-Provability
Cork, Ireland, July 2004
A preprint is available here: .ps - .dvi

Semantic Labelled Tableaux for propositional BI (without bottom).
D. Galmiche and D. Mery
Journal of Logic and Computation, vol. 13, n. 5, 2003
A preprint is available here: .ps - .dvi

A Separation Logic for Resource Distribution.
N. Biri and D. Galmiche
23rd Conference on Foundations of Software Technology
and Theoretical Computer Science, FSTTCS'03
Bombay, India, December 2003.
A preprint is available here: .ps - .dvi

Connection-based proof construction in Non-Commutative Logic.
D. Galmiche and J.M. Notin
Int. Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR'03,
Almaty, Kazakhstan, September 2003.
A preprint is available here: .ps - .dvi

Resource Tableaux (extended abstract).
D. Galmiche, D. Mery and D. Pym
Int. Conference on Computer Science Logic, CSL'02
Edinburgh, Scotland, September 2002.
A preprint is available here: .ps - .dvi

LINK: a Proof Environment based on Proof nets.
L. Habert, D. Galmiche and J.M. Notin
Int. Conference on Tableaux and Related Methods, Tableaux'02
Copenhagen, Danemark, July 2002.
A preprint is available here: .ps - .dvi

Connection-based proof search in propositional BI logic.
D. Galmiche and D. Mery
Int. Conference on Automated Deduction, CADE'02
Copenhagen, Danemark, July 2002.
A preprint is available here: .ps - .dvi

A Modal Linear Logic for Distribution and Mobility (abstract).
N. Biri and D. Galmiche
Int. Workshop on Linear Logic, WLL'02
Copenhagen, Danemark, July 2002.
A preprint is available here: .ps - .dvi

Based-on dependency Calculi for Non-commutative Logic.
D. Galmiche and J.M. Notin
Extended version of LCCS'01 paper, october 2001.
A preprint is available here: .ps - .dvi

Proof-search and Countermodel Generation in Propositional BI Logic.
D. Galmiche and D. Mery
International Symposium on Theoretical Aspects of Computer Software, TACS 2001
Tohoku University, Sendai, Japan, October 2001.
A preprint is available here: .ps - .dvi

Calculi with dependency relations for Mixed Linear Logic.
D. Galmiche and J.M. Notin
International Workshop on Logic and Complexity in Computer Science, LCCS 2001
Creteil, France, September 2001
A preprint is available here: .ps - .dvi

STRIP: Structural Sharing for Efficient Proof-search.
D. Larchey-Wendling, D. Mery and D. Galmiche
International Joint Conference on Automated Reasoning, IJCAR 2001,
Siena, Italy, 2001.
A preprint is available here: .ps - .dvi

Proof-search and Proof nets in Mixed Linear Logic.
D. Galmiche and J.M. Notin
Electronic Notes in Theoretical Computer Science , vol 37, 2000
A preprint is available here: .ps - .dvi

Labelled Proof Systems for Intuitionistic Provability
V. Balat and D. Galmiche
Labelled Deduction , Applied Logic Series, vol.17, Kluwer Academic Publisher, 2000
A preprint is available here: .ps - .dvi

Proof-search in Type-theoretic Languages: An introduction
D. Galmiche and D. Pym.
Theoretical Computer Science , vol. 232, pp 5-53, 2000.
A preprint is available here: .ps - .dvi

Quantales as completions of ordered monoids: Revised semantics for Intuitionistic Linear Logic.
D. Galmiche and D. Larchey-Wendling
Electronic Notes in Theoretical Computer Science , vol 35, 2000
A preprint is available here: .ps - .dvi

Connection methods in linear logic and proof nets construction
D. Galmiche.
Theoretical Computer Science , vol. 232, pp 231-272, 2000.
A preprint is available here: .ps - .dvi