Proof Automation and RepresenTation:
a fOundation of compUtation and deducTion

Team presentation

The PARTOUT project is interested in the principles of deductive and computational formalisms. In the broadest sense, we are interested in the question of trustworthy and verifiable meta-theory.

At one end, PARTOUT  works on the question of the essential nature of deductive or computational formalisms. For instance, we are interested in the question of proof identity that attempts to answer the following question: when are two proofs of the same theorem the same? Surprisingly, this very basic question is left unanswered in proof theory, the branch of mathematics that supposedly treats proofs as algebraic objects of interest. We also pay particular attention to the combinatorial and complexity-theoretic properties of the formalisms.

From another end, PARTOUT investigates the well studied foundational questions of the meta-theory of logical systems and type systems: cut-elimination and focusing in proof theory, type soundness and normalization theorems in type theory, etc. The focus of our research here is on the fundamental relationships behind the the notions of computation and deduction. We are particularly interested in relationships that go beyond the well known Curry-Howard correspondences between proofs and programs. Indeed, interpreting computation in terms of deduction (as in logic programming) or deduction in terms of computation (as in rewrite systems or in model checking) can often lead to fruitful and enlightening research questions, both theoretical and practical.

PARTOUT  is a joint team between Inria, Research Center Saclay- Île-de-France and LIX, École Polytechnique.