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