Professor of Computer Science
Université de Lorraine

Scientific leader TYPES Group,

Director of the Master Programme in Computer Science
Université de Lorraine

Local Director of the European Masters in Dependable Software Systems (DESEM) Master Programme

Post: LORIA - Université de Lorraine
Campus Scientifique, BP 239
54506 Vandoeuvre-les-Nancy Cedex
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 (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

Logical modelling of concepts and systems

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