Department 2 : Formal methods

Team leader : Didier Galmiche
Tél. : +33 3 83 59 20 15
Mail : didier.galmiche@loria.fr

Website

Presentation

The TYPES scientific project (Logic, Proof Theory and Programming) consists in studying the links between logic and reliable programming within the general context of designing reliable data processing systems. The relationships between computation and logic are re- garded 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). Our main goal is to study the foundations of new resource models, and related logics. Reasoning about resources and their evolution is essential to design systems (networks, servers) or programs that access memory and manipulate data structures.

Research activities

• Models, semantics and expressivity
• Proofstructures,proofs refutations and decidability

Software

• LC
• Bi-instutionistic

Collaborations

• Stéphane Demri (ENS Cachan)
• LILAC Team of IRIT (Toulouse)
• Bath University
• Roy Dyckhoff  St-Andrew University (Écosse)

Keywords

Logic, semantics, models, proofs, refutations, programs, resources