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.