### Didier GALMICHE

Post: LORIA - Université de Lorraine

Campus Scientifique, BP 239

54506 Vandoeuvre-les-Nancy Cedex

France

Email:
Didier.Galmiche@loria.fr

Phone: +33 (0) 3 83 59 20 15

Fax: +33 (0) 3 83 41 30 79

Secretary: Martine Kuhlmann

Phone: +33 (0) 3 83 59 20 51

Email: martine.kuhlmann@loria.fr

### Publications

PUBLICATIONS (since 1999)

PUBLICATIONS (before 1999)

### Research activities (TYPES group)

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 programming)

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.

### Software (TYPES
group)

IBiS :
an interactive proof assistant for bi-intuitionistic propositional logic.

SigBi (IWIL) :
a Prolog sigma-binding solver for bi-intuitionistic resource graphs.

STRIP : a theorem
prover for intuitionistic propositional logic.

LINK : a proof
environment for multiplicative linear logics.

BILL : an automated
theorem prover for the propositional fragment of the logic
of bunched implications (BI).