Authors: Santo, José Espírito
Ghilezan, Silvia 
Title: Characterization of strong normalizability for a sequent lambda calculus with co-control
Journal: ACM International Conference Proceeding Series
Volume: Part F131196
First page: 163
Last page: 174
Conference: 19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017; Namur; Belgium; 9 October 2017 through 11 October 2017
Issue Date: 9-Oct-2017
ISBN: 978-1-450-35291-8
DOI: 10.1145/3131851.3131867
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.
Keywords: Bidirectional natural deduction | Co-control | Intersection types | Sequent calculus | Strong normalization
Publisher: Association for Computing Machinery
Project: FCT - Fundação para a Ciência e a Tecnologia, project UID-MAT-00013/2013
Representations of logical structures and formal languages and their application in computing 
Development of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education 

Show full item record


checked on May 16, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.