Didier GALMICHE

Research Group TYPES

Logic, Proof Theory and Programming

LORIA UMR 7503

Members

Research activities

The TYPES scientific project (Logic, Proof Theory and Programming) consists in considering the links between logic
and reliable programming within the general context of designing reliable data processing systems. The relationships
between computation and logic are regarded as fundamental, as perceived through paradigms of programming such as
proofs-as-programs (Curry-Howard isomorphism, functional programming), proofs-as-computations (logic program-
ming) and proofs-as-processes (concurrent programming). Accordingly, modelling of concepts, mechanisms and
computations is approached through logic (proof theory and semantics) using methods based on automatized construction
of proofs and structural analysis in substructural and constructive logics.

Proof-search methods and analysis

Constructive and substructural logics (classical, intuitionistic, linear logics), type theory and programming (algorithmic contents of proofs).
Proof systems (sequent calculi, proof nets, labelled calculi), proof-search methods, implementation techniques (resource management, sharing).
Semantics and provability, completeness, refutation, counter-models generation.

Logical modelling of concepts and systems

Specification logics - concepts (non-determinism, concurrency, distribution, sequentiality), - systems (concurrent, reactive, distributed).
Nets, processes, concurrent objects.
Proofs of properties, synthesis and verification of programs.

Some recent results

- Definition of semantic calculi for propositional Bunched Implications logic (BI) and of related methods (tableaux, connections)
based on labels and constraints. Proofs of soundness and completeness of these calculi w.r.t. resource semantics, with an
emphasis on countermodels construction.
- Decidability of propositional BI and the finite model property with respect to topological semantics. Definition of a new semantics,
based on partially defined monoids, which generalizes the semantics of BI's (classical and intuitionistic) pointer logic and for which
BI is complete.
- Definition of a new calculus (and the related method) for deciding Goedel-Dummett logic, that is based on a particular combination
of proof-search and counter-model construction.
- Definition of a new separation logic, extension of BI with a modality for locations, and a resource model based on a new structure
called resource tree. Study of the decidability by model checking and theorem proving of satisfaction and validity in this separation logic
- Definition of a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL) and its intuitionistic
fragment (IMNL). New algorithms for proof nets construction in both logical fragments.

Software

STRIP

STRIP is a theorem prover for IPL (Intuitionistic Propositional Logic) developed in the TYPES group
and is available from the STRIP Web page .
Its main characteristic is to eliminate formulae duplication during proof-search by structural sharing.
Moreover it builds counter-models in case of non-provability.
The proof-theoretic foundations are presented in the following paper
- Structural sharing and efficient proof-search in propositional intuitionistic logic .
Asian Computing Science Conference, ASIAN'99, LNCS 1742, Phuket, Thailand, 1999.
- STRIP: Structural Sharing for Efficient Proof-search. .
First International Joint Conference on Automated Reasoning, IJCAR 2001, LNCS 2083, Siena, Italy, 2001.

LINK

LINK is a proof environment for Multiplicative Linear Logic (MLL), Non-Commutative or Cyclic MLL
(MCyLL) and Mixed MLL or Non-Commutative Logic (MNL), developed in the TYPES group.
It is based on algorithms for proof nets construction in these logics
and is available from the LINK Web page .
The proof-theoretic foundations are presented in the following papers:
- Proof nets Construction and Automated Deduction in Non-commutative Linear Logic .
Electronic Notes in Theorical Computer Science, vol 17, 1998.
- Proof-search and Proof nets in Mixed Linear Logic. .
Electronic Notes in Theorical Computer Science, vol 37, 2000.
- Calculi with dependency relations for Mixed Linear Logic .
Int. Workshop on Logic and Complexity in Computer Science, LCCS 2001,
Creteil, France, September 2001.
- LINK: a Proof Environment based on Proof Nets. .
Int. Conference on Analytic Tableaux and Related Methods, TABLEAUX'02,
LNCS 2381, Copenhagen, Danemark, July 2002.

BILL

BILL is an automated theorem prover for the propositional fragment of BI, the Logic of Bunched Implications.
It is based on a new tableau method for BI that is based on labels and label constraints
and it is available from the BILL Web page .
The proof-theoretic foundations are presented in the following papers:
- Proof-search and Countermodel Generation in Propositional BI Logic .
Int. Symposium on Theoretical Aspects of Computer Software, TACS 2001,
LNCS 2215, Sendai, Japan, October 2001.
- Resource Tableaux (extended abstract) .
Int. Conference on Computer Science Logic, CSL'02,
LNCS 2471, Edinburgh, Scotland, September 2002.