Didier Galmiche

Professor of Computer Science
Université Henri Poincaré - Nancy 1

Scientific leader TYPES Group,
LORIA UMR 7503


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

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