Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/50671
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | por |
dc.contributor.author | Ghilezan, Silvia | por |
dc.date.accessioned | 2018-02-20T09:16:36Z | - |
dc.date.available | 2018-02-20T09:16:36Z | - |
dc.date.issued | 2017 | - |
dc.identifier.isbn | 9781450352918 | por |
dc.identifier.uri | https://hdl.handle.net/1822/50671 | - |
dc.description.abstract | 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. | por |
dc.description.sponsorship | The authors would like to thank the anonymous referees for their valuable comments and helpful suggestions. This work was partly supported by FCT—Fundação para a Ciência e a Tecnologia, within the project UID-MAT-00013/2013; by COST Action CA15123 - The European research network on types for programming and verification (EUTypes) via STSM; and by the Ministry of Education, Science and Technological Development, Serbia, under the projects ON174026 and III44006. | por |
dc.language.iso | eng | por |
dc.publisher | ACM | por |
dc.rights | openAccess | por |
dc.subject | Intersection types | por |
dc.subject | Strong normalization | por |
dc.subject | Sequent calculus | por |
dc.subject | Bidirectional natural deduction | por |
dc.subject | Co-control | por |
dc.title | Characterization of strong normalizability for a sequent lambda calculus with co-control | por |
dc.type | conferencePaper | por |
dc.peerreviewed | yes | por |
oaire.citationConferenceDate | 09 - 11 nov. 2017 | por |
sdum.event.type | other | por |
oaire.citationStartPage | 163 | por |
oaire.citationEndPage | 174 | por |
oaire.citationConferencePlace | Namur, Belgium | por |
oaire.citationVolume | Part F131196 | por |
dc.identifier.doi | 10.1145/3131851.3131867 | por |
dc.description.publicationversion | info:eu-repo/semantics/publishedVersion | por |
dc.subject.wos | Science & Technology | por |
sdum.conferencePublication | PPDP '17 Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming | por |
sdum.bookTitle | PROCEEDINGS OF THE 19TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2017) | por |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
espirito-santo-23.pdf | 759,29 kB | Adobe PDF | Ver/Abrir |