Please use this identifier to cite or link to this item:

TitlePermutability in proof terms for intuitionistic sequent calculus with cuts
Author(s)Espírito Santo, José
Frade, M. J.
Pinto, Luís F.
KeywordsSequent calculus
Permutative conversion
Curry-Howard isomorphism
Vector of arguments
Generalized application
Normal proof
Natural proof
Cut elimination
Issue date2018
PublisherSchloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH
JournalLeibniz International Proceedings in Informatics, Lipics
Abstract(s)This paper gives a comprehensive and coherent view on permutability in the intuitionistic sequent calculus with cuts. Specifically we show that, once permutability is packaged into appropriate global reduction procedures, it organizes the internal structure of the system and determines fragments with computational interest, both for the computation-as-proof-normalization and the computation-as-proof-search paradigms. The vehicle of the study is a lambda-calculus of multiary proof terms with generalized application, previously developed by the authors (the paper argues this system represents the simplest fragment of ordinary sequent calculus that does not fall into mere natural deduction). We start by adapting to our setting the concept of normal proof, developed by Mints, Dyckhoff, and Pinto, and by defining natural proofs, so that a proof is normal iff it is natural and cut-free. Natural proofs form a subsystem with a transparent Curry-Howard interpretation (a kind of formal vector notation for lambda-terms with vectors consisting of lists of lists of arguments), while searching for normal proofs corresponds to a slight relaxation of focusing (in the sense of LJT). Next, we define a process of permutative conversion to natural form, and show that its combination with cut elimination gives a concept of normalization for the sequent calculus. We derive a systematic picture of the full system comprehending a rich set of reduction procedures (cut elimination, flattening, permutative conversion, normalization, focalization), organizing the relevant subsystems and the important subclasses of cut-free, normal, and focused proofs.
TypeConference paper
AccessOpen access
Appears in Collections:CMAT - Artigos em atas de conferências e capítulos de livros com arbitragem / Papers in proceedings of conferences and book chapters with peer review
HASLab - Artigos em atas de conferências internacionais (texto completo)

Files in This Item:
File Description SizeFormat 
LIPIcs-TYPES-2016-10(ThePublishedVersion).pdf623,79 kBAdobe PDFView/Open

This item is licensed under a Creative Commons License Creative Commons

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID