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


JOURNAL, CONFERENCE, WOKSHOP PAPERS (since 1999)


A Substructural Epistemic Resource Logic
D. Galmiche and P. Kimmel and D. Pym
Seventh Indian Conference on Logic and its Applications, ICLA 2017
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, vol. 637, pp 30-58, 2016
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, 2016
A preprint is available here: .pdf


About Intuitionistic Public Announcement Logic
Ph. Balbiani and D. Galmiche
Int. Conf. on Advances in Modal Logic, AiML 2016
Budapest, Hungary, August 2016
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, 2015
A preprint is available here: .pdf


A Modal Separation Logic for Resource Dynamics
J-R. Courtault and D. Galmiche
Journal of Logic and Computation, 2015
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 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


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


Resource models and proof-search in Intuitionistic Linear Logic.
D. Larchey-Wendling and D. Galmiche
A preprint is available here: .ps - .dvi


Structural sharing and efficient proof-search in propositional intuitionistic logic
D. Galmiche and D. Larchey-Wendling
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 Vandoeuvre-les-Nancy, 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