PARSIFAL Research team

Proof search and reasoning with logic specifications

Team presentation

The PARSIFAL project-team aims at elaborating methods and tools for specifying and reasoning about computation systems, such as, for example, compilers, security protocols, and concurrent programs. A central challenge here is proving properties of programs that manipulate other programs.

The specification of computation systems today is commonly given using operational semantics, which are generally given via inference rules over relations. Such inference rules are also used for specifying the static semantics for programming languages (type inference, for example).

This project will exploit recent developments in proof theory, logic programming, and type theory to animate and reason about operational semantics specifications.

Research themes

  • Foundations: We plan to exploit proof search in rich logics for the specification of computations and to develop a single logic for reasoning about proof search specifications. This logic will be based on higher-order intuitionistic logic and will include proof principles for induction and co-induction. We shall also consider its analogous design as a type system.
  • Applications: Our work will be targeted at developing component technology for deduction that can be used to build model checkers, symbolic bisimulation checkers, type checkers, proof checkers, specialized theorem provers, etc. Such deductive tools will be incorporated into other systems to support deduction during computation. Typical applications we have in mind are in the area of security, global computing, proof-carrying code, and mobile code.
  • Prototypes: We plan to develop various components needed for the implementation of proof search (including unification, search, tabling, binding and substitution in syntax, etc) and use these components to build specific research prototypes for a range of applications that mix computation and deduction.

International and industrial relations

  • RAPT (Recent Advances in Proof Theory) is an "Equipes Associées" with seed money from INRIA. International collaborators on this project are Brigitte Pientka at McGill University in Montreal and Frank Pfenning at Carnegie Mellon University in Pittsburgh.
  • Mobius (Mobility, Ubiquity and Security) is an Integrated European Project launched under the FET Global Computing Proactive Initiative.
  • Slimmer (Sophisticated logic implementations for modeling and mechanical reasoning) is an "Equipes Associées" with seed money from INRIA. Gopalan Nadathur from the University of Minnesota has received matching money from NSF for this effort.
  • Vallauris is a PAI ("les programmes d'actions intégrées") within Programme Picasso 2005 of Égide. The Vallauris project's scientific title is "Integrating Proof Theoretic techniques and Semantic Tools in Proof Carrying Code and Validation and Analysis of Declarative code".
  • Rossignol is an "ACI-Securité" project that deals with the verification of cryptographic protocols.
  • GeoCal is an "ACI-Nouvelles interfaces des mathematiques project". GeoCal collects together 10 research teams in logic, theoretical computer science, and algebraic topology.
  • The Types European project is the continuation of a series of previous Types projects dating back to 1992. The project collects together 35 sites aiming at developing the technology of formal reasoning and computer programming based on Type Theory.

Research teams of the same theme :

Inria Headquarters and research centres

Direct links

Social