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.