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):892922, 2021.
https://doi.org/10.1093/logcom/exab017
A preprint is available here:
.pdf


Relating Labelled and Labelfree 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 130146, 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): 12511287, 2019.
A preprint is available here:
.pdf


A Public Announcement Separation Logic
JR. Courtault and H. van Ditmarsch and D. Galmiche
Mathematical Structures in Computer Science, 29(6):828871,
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
NonClassical Logics, EICNCL 2018
Oxford, UK, July 2018
A preprint is available here:
.pdf


Labelled Connectionbased Proof Search for Multiplicative
Intuitionistic Linear Logic
D. Galmiche and D. Mery
3rd Int. Workshop on Automated Reasoning in
Quantified
NonClassical 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
JR. Courtault and D. Galmiche
Journal of Logic and Computation, 28(4): 733778, 2018.
A preprint is available here:
.pdf


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


Separation Logic with One Quantified Variable
S. Demri and D. Galmiche and D. LarcheyWendling and D. Mery
Theory of Computing Systems, (ToCS), 61(2):371461,
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 7791
Kanpur, India, January 2017
A preprint is available here:
.pdf


A logic of Separating Modalities
JR. Courtault and D. Galmiche and D. Pym
Theoretical Computer Science, 637:3058, 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,
pp97116
Budapest, Hungary, August 2016
A preprint is available here:
.pdf


An Epistemic Separation Logic
JR. 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 BIeyes
D. LarcheyWendling 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. LarcheyWendling and D. Mery
Int. Computer Science Symposium in Russia, CSR 2014
Moscow, Russia, June 2014
A preprint is available here:
.pdf


A Connectionbased Characterization of Biintuitionistic Validity
D. Galmiche and D. Mery
Journal of Automated Reasoning, vol. 51, 2013
A preprint is available here:
.pdf


Nondeterministic Phase Semantics and the Undecidability of
Boolean BI
D. LarcheyWendling and D. Galmiche
ACM Transactions on Computational Logic, vol. 14, 2013
A preprint is available here:
.pdf


An Interactive Prover for Biintuitionistic Logic
JR. 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
JR. 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
JR. 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 Connectionbased Characterization of Biintuitionistic Validity
D. Galmiche and D. Mery
Int. Conference on Automated Deduction, CADE23
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 14471463, 2011
A preprint is available here:
.pdf


Some Remarks on Relations between Proofs and Games
D. Galmiche and D. LarcheyWendling and J. VidalRosset
Construction  Festschrift for Gerhard Heinzmann
editors P.E. Bour, M. Rebushi, L. Rollet, pp 397410, College Publications, 2010
A preprint is available here:
.pdf


Labelfree 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 373421, 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 371385, 2010
A preprint is available here:
.pdf


The Undecidability of Boolean BI through Phase Semantics
D. LarcheyWendling 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


Labelfree Proof Systems for Intuitionistic Modal Logic IS5
D. Galmiche and Y. Salhi
Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR16
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 189231, 2010.
A preprint is available here:
.ps 
.pdf


Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
D. LarcheyWendling 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 687726, 2007
A preprint is available here:
.ps 
.pdf


Provability and Countermodels in GoedelDummett Logics
D. Galmiche and D. LarcheyWendling and Y. Salhi
Int. Workshop on Disproving, Nontheorems, Nonvalidity, NonProuvability, DISPROVING'07,
Bremen, Germany, July 2007.
A preprint is available here:
.ps 
.pdf


Connectionbased 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. LarcheyWendling
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 10331088, 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: NonTheorems, Nonvalidity,
NonProvability
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


Connectionbased proof construction in NonCommutative 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


Connectionbased 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


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


Proofsearch 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 Proofsearch.
D. LarcheyWendling, D. Mery and D. Galmiche
International Joint Conference on Automated Reasoning, IJCAR
2001,
Siena, Italy, 2001.
A preprint is available here:
.ps 
.dvi


Proofsearch 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


Proofsearch in Typetheoretic Languages: An introduction
D. Galmiche and D. Pym.
Theoretical Computer Science , vol. 232, pp 553, 2000.
A preprint is available here:
.ps 
.dvi


Quantales as completions of ordered monoids: Revised
semantics for Intuitionistic Linear Logic.
D. Galmiche and D. LarcheyWendling
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 231272, 2000.
A preprint is available here:
.ps 
.dvi


A Specification Logic for Concurrent ObjectOriented Programming
G. Delzanno, D. Galmiche and M. Martelli.
Mathematical Structures in Computer Science , vol. 9, n. 3, pp 253286, 1999.
A preprint is available here:
.ps


Resource models and proofsearch in Intuitionistic Linear Logic.
D. LarcheyWendling and D. Galmiche
A preprint is available here:
.ps 
.dvi


Structural sharing and efficient proofsearch in
propositional intuitionistic logic
D. Galmiche and D. LarcheyWendling
Asian Computing Science Conference, ASIAN'99, LNCS 1742
, Phuket, Thailand, 1999.
A preprint is available here:
.ps 
.dvi

Further information:
Didier Galmiche
LORIA UMR 7503  UHP Nancy 1
Campus Scientifique  BP 239
54506 VandoeuvrelesNancy, France
Email: Didier.Galmiche@loria.fr
Direct phone: +33 (0)3 83 59 20 15
Fax: +33 (0)3 83 41 30 79
URL: http://www.loria.fr/~galmiche