Research Group TYPES - CRIN-CNRS and INRIA Lorraine
Type theories, Proof search, Computational aspects of proof theory
Objectives
The scientific project of TYPES is involved in the general approach to
the design of correct systems through the links between logic and
programming. We consider the relationship between programs and proofs
such it appears in two programming paradigms: proofs-as-programs
(Curry-Howard isomorphism) and proof-search-as-computation as fundamental.
Thus, we modelize concepts and calculi through logic (proof theory, semantics)
with methods based on the analysis of proofs and on the automatized proof
construction (search) in constructive logics.
Topics
- Analysis and representation of programming concepts into logic
(proof theory, semantics).
- Non-determinism and control in sequential and concurrent
systems.
- Methods for the analysis and the construction of proofs in
adequate frameworks for concepts design and systems specification
(type theory, linear logic and typed lambda-calculi).
- Proof environments based on these methods and tools (for
verification, synthesis) and applications.