Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/26886
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | - |
dc.contributor.author | Ivetic, J, | - |
dc.contributor.author | Likavec, Silvia | - |
dc.date.accessioned | 2013-12-10T17:46:29Z | - |
dc.date.available | 2013-12-10T17:46:29Z | - |
dc.date.issued | 2012 | - |
dc.identifier.issn | 0169-2968 | por |
dc.identifier.uri | https://hdl.handle.net/1822/26886 | - |
dc.description.abstract | This paper gives a characterisation, via intersection types, of the strongly normalising proof-terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary lambdal-calculus. The completeness of the typing system is obtained from subject expansion at root position. Next we use our result to analyze the characterisation of strong normalisability for three classes of intuitionistic terms: ordinary lambda-terms, LambdaJ-terms (lambda-terms with generalised application), and lambdax-terms (lambda-terms with explicit substitution). We explain via our system why the type systems iin the natural deduction format for LambdaJ and lambdax known from the literature contain extra, exceptional rules for typing generalised application or substitution; and we show a new characterisation of the beta-strongly normalising l-terms, as a corollary to a PSN-result, relating the lambda-calculus and the intuitionistic sequent calculus. Finally, we obtain variants of our characterisation by restricting the set of assignable types to sub-classes of intersection types, notably strict types. In addition, the known characterisation of the beta-strongly normalising lambda-terms in terms of assignment of strict types follows as an easy corollary of our results. | por |
dc.description.sponsorship | Fundação para a Ciência e Tecnologia | por |
dc.language.iso | eng | por |
dc.publisher | IOS Press | por |
dc.rights | openAccess | por |
dc.subject | Sequent calculus | por |
dc.subject | Strong normalisation | por |
dc.subject | Intersection types | por |
dc.subject | Intuitionistic logic | por |
dc.title | Characterising strongly normalising intuitionistic terms | por |
dc.type | article | por |
dc.peerreviewed | yes | por |
sdum.publicationstatus | published | por |
oaire.citationStartPage | 83 | por |
oaire.citationEndPage | 120 | por |
oaire.citationIssue | 1-4 | por |
oaire.citationTitle | Fundamenta Informaticae | por |
oaire.citationVolume | 121 | por |
dc.identifier.doi | 10.3233/FI-2012-772 | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Fundamenta Informaticae | por |
Aparece nas coleções: | CMAT - Artigos em revistas com arbitragem / Papers in peer review journals |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
FI-esil(versaoRepositorium).pdf | 287,89 kB | Adobe PDF | Ver/Abrir |