### Didier Galmiche

Post: LORIA - Universite Henri Poincare

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: Josiane Reffort

Phone: +33 (0) 3 83 59 30 65

Email: reffort@loria.fr

### Publications

RECENT
PUBLICATIONS

LESS RECENT
PUBLICATIONS

### 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).