Parsifal

Research topics

The specification of computation systems today is commonly given using operational semantics, supplanting the well-established but restrictive approach using denotational semantics. Operational semantics is generally given via inference rules using relations between different items of the computation, and for this reason, it is an example of a relational specification. Inference rules over relations are also used for specifying the static semantics for programming languages as well (type inference, for example).

The use of denotational style presentations of computational systems naturally leads to the use of functional programming-based executable specifications. Similarly, the use of inference systems for the presentation of operational semantics provides a natural setting for exploiting logic programming-based implementations.

The Parsifal project will exploit recent developments in proof search and logic programming to make the specification of operational semantics more expressive and declarative and will develop techniques and tools for reasoning directly on logic-based specifications.

More specifically, the Parsifal project will focus on the following goals.

Theoretical goals

1. Illustrate the value of using rich proof search specifications logics for the specification of computations.
2. Develop a single logic for reasoning about proof search specifications based on higher-order intuitionistic logic and including induction and co-induction proof principles; also consider its analogous design as a type system.

Implementation goals

1. Develop various components needed for the implementation of proof search (including unification, search, tabling, binding and substitution in syntax, etc).
2. Build specific prototypes for a range of applications, such as those that mix computation and deduction. Eventually develop a prototype interactive theorem prover that allows meta-theoretical properties of operational systems to be established.

Application goals

1. Develop component technology for deduction that might be incorporated into other systems to support deduction during computation: global computing, security, proof-carrying code, mobile code, etc.
2. Develop typical applications of the systems above: specifically, model checkers, symbolic bisimulation, type inference, proof checking, specialized theorem provers, etc.

Members

• Beniamino Accattoli
• Ryuta Arisaka
• Kaustuv Chaudhuri
• Mahfuza Farooque
• Ivan Gazeau
• Nicolas Guenot
• Willem Heijltjes
• Hichem Chihani
• Clement Houtmann
• Salil Joshi
• Francois Lamarche
• Stephane Lengrand
• Christelle Lievin
• Chris Martens
• Cimini Matteo
• Dale Miller
• Anne-Laure Poupon
• Revantha Ramanayake
• Mikheil Rukhaia
• Lutz Strassburger
• Xiao Wang