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 program-

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

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

- Specification logics

- concepts (non-determinism, concurrency, distribution, sequentiality),

- systems (concurrent, reactive, distributed). - Nets, processes, concurrent objects.
- Proofs of properties, synthesis and verification of programs.

based on labels and constraints. Proofs of soundness and completeness of these calculi w.r.t. resource semantics, with an

emphasis on countermodels construction.

- Decidability of propositional BI and the finite model property with respect to topological semantics. Definition of a new semantics,

based on partially defined monoids, which generalizes the semantics of BI's (classical and intuitionistic) pointer logic and for which

BI is complete.

- Definition of a new calculus (and the related method) for deciding Goedel-Dummett logic, that is based on a particular combination

of proof-search and counter-model construction.

- Definition of a new separation logic, extension of BI with a modality for locations, and a resource model based on a new structure

called resource tree. Study of the decidability by model checking and theorem proving of satisfaction and validity in this separation logic

- Definition of a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL) and its intuitionistic

fragment (IMNL). New algorithms for proof nets construction in both logical fragments.

and is available from the STRIP Web page .

Its main characteristic is to eliminate formulae duplication during proof-search by structural sharing.

Moreover it builds counter-models in case of non-provability.

The proof-theoretic foundations are presented in the following paper

- Structural sharing and efficient proof-search in propositional intuitionistic logic .

Asian Computing Science Conference, ASIAN'99, LNCS 1742, Phuket, Thailand, 1999.

- STRIP: Structural Sharing for Efficient Proof-search. .

First International Joint Conference on Automated Reasoning, IJCAR 2001, LNCS 2083, Siena, Italy, 2001.

(MCyLL) and Mixed MLL or Non-Commutative Logic (MNL), developed in the TYPES group.

It is based on algorithms for proof nets construction in these logics

and is available from the LINK Web page .

The proof-theoretic foundations are presented in the following papers:

- Proof nets Construction and Automated Deduction in Non-commutative Linear Logic .

Electronic Notes in Theorical Computer Science, vol 17, 1998.

- Proof-search and Proof nets in Mixed Linear Logic. .

Electronic Notes in Theorical Computer Science, vol 37, 2000.

- Calculi with dependency relations for Mixed Linear Logic .

Int. Workshop on Logic and Complexity in Computer Science, LCCS 2001,

Creteil, France, September 2001.

- LINK: a Proof Environment based on Proof Nets. .

Int. Conference on Analytic Tableaux and Related Methods, TABLEAUX'02,

LNCS 2381, Copenhagen, Danemark, July 2002.

It is based on a new tableau method for BI that is based on labels and label constraints

and it is available from the BILL Web page .

The proof-theoretic foundations are presented in the following papers:

- Proof-search and Countermodel Generation in Propositional BI Logic .

Int. Symposium on Theoretical Aspects of Computer Software, TACS 2001,

LNCS 2215, Sendai, Japan, October 2001.

- Resource Tableaux (extended abstract) .

Int. Conference on Computer Science Logic, CSL'02,

LNCS 2471, Edinburgh, Scotland, September 2002.