Section: Overall Objectives

Main themes

The aim of the Parsifal team is to develop and exploit proof theory and type theory in the specification, verification, and analysis of computational systems.

• Expertise: the team conducts basic research in proof theory and type theory. In particular, the team is developing results that help with automated deduction and with the manipulation and communication of formal proofs.

• Design: based on experience with computational systems and theoretical results, the team develops new logical principles, new proof systems, and new theorem proving environments.

• Implementation: the team builds prototype systems to help validate basic research results.

• Examples: the design and implementation efforts are guided by examples of specification and verification problems. These examples not only test the success of the tools but also drive investigations into new principles and new areas of proof theory and type theory.

The foundational work of the team focuses on structural and analytic proof theory, i.e., the study of formal proofs as algebraic and combinatorial structures and the study of proof systems as deductive and computational formalisms. The main focus in recent years has been the study of the sequent calculus and of the deep inference formalisms.

An important research question is how to reason about computational specifications that are written in a relational style. To this end, the team has been developing new approaches to dealing with induction, co-induction, and generic quantification. A second important question is of canonicity in deductive systems, i.e., when are two derivations “essentially the same”? This crucial question is important not only for proof search, because it gives an insight into the structure and an ability to manipulate the proof search space, but also for the communication of proof objects between different reasoning agents such as automated theorem provers and proof checkers.

Important application areas currently include:

• Meta-theoretic reasoning on functional programs, such as terms in the $\lambda$-calculus

• Reasoning about behaviors in systems with concurrency and communication, such as the $\pi$-calculus, game semantics, etc.

• Combining interactive and automated reasoning methods for induction and co-induction

• Verification of distributed, reactive, and real-time algorithms that are often specified using modal and temporal logics

• Representing proofs as documents that can be printed, communicated, and checked by a wide range of computational logic systems.

• Development of cost models for the evaluation of proofs and programs.