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 :
Theses
Complete list of metadatas

Cited literature [113 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00929908
Contributor : Nicolas Guenot <>
Submitted on : Wednesday, April 23, 2014 - 5:50:26 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Long-term archiving on : Saturday, April 8, 2017 - 3:04:30 PM

Identifiers

  • HAL Id : pastel-00929908, version 1

Collections

Citation

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

Share

Metrics

Record views

314

Files downloads

296