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

TitleCharacterization of strong normalizability for a sequent lambda calculus with co-control
Author(s)Espírito Santo, José
Ghilezan, Silvia
KeywordsIntersection types
Strong normalization
Sequent calculus
Bidirectional natural deduction
Issue date2017
Abstract(s)We study strong normalization in a lambda calculus of proof-terms with co-control for the intuitionistic sequent calculus. In this sequent lambda calculus, the management of formulas on the left hand side of typing judgements is “dual" to the management of formulas on the right hand side of the typing judgements in Parigot’s lambdamu calculus - that is why our system has first-class “co-control". The characterization of strong normalization is by means of intersection types, and is obtained by analyzing the relationship with another sequent lambda calculus, without co-control, for which a characterization of strong normalizability has been obtained before. The comparison of the two formulations of the sequent calculus, with or without co-control, is of independent interest. Finally, since it is known how to obtain bidirectional natural deduction systems isomorphic to these sequent calculi, characterizations are obtained of the strongly normalizing proof-terms of such natural deduction systems.
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

Files in This Item:
File Description SizeFormat 
espirito-santo-23.pdf759,29 kBAdobe PDFView/Open

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