Skip to Main content Skip to Navigation

Nested Deduction in Logical Foundations for Computation

Nicolas Guenot 1 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : This thesis investigates the use of deep inference formalisms as basis for a computational interpretation of proof systems, following the two main approaches: proofs-as-programs and proof-search-as-computation. The first contribution is the development of a family of proof systems for intuitionistic logic in the calculus of structures and in nested sequents, for which internal normalisation procedures are given. One of these procedure is then interpreted in terms of computation, as a refinement of the Curry-Howard correspondence allowing to introduce a form of sharing and communication operators in a lambda-calculus with explicit substitution. On the side of proof-search, the notion of focused proof in linear logic is transferred from the sequent calculus into the calculus of structures, where it yields an incremental form of focusing, with a simple proof of completeness. Finally, another interpretation of proof-search is given through the encoding of reduction in a lambda-calculus with explicit substitution into the inference rules of a subsystem of intuitionistic logic in the calculus of structures.
Document type :
Complete list of metadata

Cited literature [113 references]  Display  Hide  Download
Contributor : Nicolas Guenot Connect in order to contact the contributor
Submitted on : Wednesday, April 23, 2014 - 5:50:26 PM
Last modification on : Thursday, January 20, 2022 - 5:30:45 PM
Long-term archiving on: : Saturday, April 8, 2017 - 3:04:30 PM


  • HAL Id : pastel-00929908, version 1



Nicolas Guenot. Nested Deduction in Logical Foundations for Computation. Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English. ⟨pastel-00929908⟩



Record views


Files downloads