Characterising Strongly Normalising Intuitionistic Sequent Terms
Identifieur interne : 000648 ( Istex/Curation ); précédent : 000647; suivant : 000649Characterising Strongly Normalising Intuitionistic Sequent Terms
Auteurs : J. Espírito Santo [Portugal] ; S. Ghilezan [Serbie] ; J. Iveti [Serbie]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper gives a characterisation, via intersection types, of the strongly normalising 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 λ-calculus. The completeness of the typing system is obtained from subject expansion at root position. This paper’s sequent term calculus integrates smoothly the λ-terms with generalised application or explicit substitution. Strong normalisability of these terms as sequent terms characterises their typeability in certain “natural” typing systems with intersection types. The latter are in the natural deduction format, like systems previously studied by Matthes and Lengrand et al., except that they do not contain any extra, exceptional rules for typing generalised applications or substitution.
Url:
DOI: 10.1007/978-3-540-68103-8_6
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000653
Links to Exploration step
ISTEX:1CB16E50D217A5407B98673DF326F8AF7574915BLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Characterising Strongly Normalising Intuitionistic Sequent Terms</title><author><name sortKey="Espirito Santo, J" sort="Espirito Santo, J" uniqKey="Espirito Santo J" first="J." last="Espírito Santo">J. Espírito Santo</name><affiliation wicri:level="1"><mods:affiliation>Mathematics Department, University of Minho, Portugal</mods:affiliation><country xml:lang="fr">Portugal</country><wicri:regionArea>Mathematics Department, University of Minho</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: jes@math.uminho.pt</mods:affiliation><country wicri:rule="url">Portugal</country></affiliation></author><author><name sortKey="Ghilezan, S" sort="Ghilezan, S" uniqKey="Ghilezan S" first="S." last="Ghilezan">S. Ghilezan</name><affiliation wicri:level="1"><mods:affiliation>Faculty of Engineering, University of Novi Sad, Serbia</mods:affiliation><country xml:lang="fr">Serbie</country><wicri:regionArea>Faculty of Engineering, University of Novi Sad</wicri:regionArea></affiliation><affiliation><mods:affiliation>E-mail: gsilvia@uns.ns.ac.yu</mods:affiliation><wicri:noCountry code="no comma">E-mail: gsilvia@uns.ns.ac.yu</wicri:noCountry></affiliation></author><author><name sortKey="Iveti, J" sort="Iveti, J" uniqKey="Iveti J" first="J." last="Iveti">J. Iveti</name><affiliation wicri:level="1"><mods:affiliation>Faculty of Engineering, University of Novi Sad, Serbia</mods:affiliation><country xml:lang="fr">Serbie</country><wicri:regionArea>Faculty of Engineering, University of Novi Sad</wicri:regionArea></affiliation><affiliation><mods:affiliation>E-mail: jelena@imft.ftn.ns.ac.yu</mods:affiliation><wicri:noCountry code="no comma">E-mail: jelena@imft.ftn.ns.ac.yu</wicri:noCountry></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:1CB16E50D217A5407B98673DF326F8AF7574915B</idno><date when="2008" year="2008">2008</date><idno type="doi">10.1007/978-3-540-68103-8_6</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-N6KS52T8-N/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000653</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000653</idno><idno type="wicri:Area/Istex/Curation">000648</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Characterising Strongly Normalising Intuitionistic Sequent Terms</title><author><name sortKey="Espirito Santo, J" sort="Espirito Santo, J" uniqKey="Espirito Santo J" first="J." last="Espírito Santo">J. Espírito Santo</name><affiliation wicri:level="1"><mods:affiliation>Mathematics Department, University of Minho, Portugal</mods:affiliation><country xml:lang="fr">Portugal</country><wicri:regionArea>Mathematics Department, University of Minho</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: jes@math.uminho.pt</mods:affiliation><country wicri:rule="url">Portugal</country></affiliation></author><author><name sortKey="Ghilezan, S" sort="Ghilezan, S" uniqKey="Ghilezan S" first="S." last="Ghilezan">S. Ghilezan</name><affiliation wicri:level="1"><mods:affiliation>Faculty of Engineering, University of Novi Sad, Serbia</mods:affiliation><country xml:lang="fr">Serbie</country><wicri:regionArea>Faculty of Engineering, University of Novi Sad</wicri:regionArea></affiliation><affiliation><mods:affiliation>E-mail: gsilvia@uns.ns.ac.yu</mods:affiliation></affiliation></author><author><name sortKey="Iveti, J" sort="Iveti, J" uniqKey="Iveti J" first="J." last="Iveti">J. Iveti</name><affiliation wicri:level="1"><mods:affiliation>Faculty of Engineering, University of Novi Sad, Serbia</mods:affiliation><country xml:lang="fr">Serbie</country><wicri:regionArea>Faculty of Engineering, University of Novi Sad</wicri:regionArea></affiliation><affiliation><mods:affiliation>E-mail: jelena@imft.ftn.ns.ac.yu</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper gives a characterisation, via intersection types, of the strongly normalising 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 λ-calculus. The completeness of the typing system is obtained from subject expansion at root position. This paper’s sequent term calculus integrates smoothly the λ-terms with generalised application or explicit substitution. Strong normalisability of these terms as sequent terms characterises their typeability in certain “natural” typing systems with intersection types. The latter are in the natural deduction format, like systems previously studied by Matthes and Lengrand et al., except that they do not contain any extra, exceptional rules for typing generalised applications or substitution.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000648 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 000648 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:1CB16E50D217A5407B98673DF326F8AF7574915B
|texte= Characterising Strongly Normalising Intuitionistic Sequent Terms
}}
| This area was generated with Dilib version V0.6.33. |  |