Intersection Type Systems and Explicit Substitutions Calculi
Identifieur interne : 003063 ( Main/Exploration ); précédent : 003062; suivant : 003064Intersection Type Systems and Explicit Substitutions Calculi
Auteurs : Daniel Lima Ventura [Brésil] ; Mauricio Ayala-Rinc N [Brésil] ; Fairouz Kamareddine [Royaume-Uni]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: The λ-calculus with de Bruijn indices, called λ dB , assembles each α-class of λ-terms into a unique term, using indices instead of variable names. Intersection types provide finitary type polymorphism satisfying important properties like principal typing, which allows the type system to include features such as data abstraction (modularity) and separate compilation. To be closer to computation and to simplify the formalisation of the atomic operations involved in β-contractions, several explicit substitution calculi were developed most of which are written with de Bruijn indices. Although untyped and simply types versions of explicit substitution calculi are well investigated, versions with more elaborate type systems (e.g., with intersection types) are not. In previous work, we presented a version for λ dB of an intersection type system originally introduced to characterise principal typings for β-normal forms and provided the characterisation for this version. In this work we introduce intersection type systems for two explicit substitution calculi: the λσ and the λs e . These type system are based on a type system for λ dB and satisfy the basic property of subject reduction, which guarantees the preservation of types during computations.
Url:
DOI: 10.1007/978-3-642-13824-9_19
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000883
- to stream Istex, to step Curation: 000878
- to stream Istex, to step Checkpoint: 000825
- to stream Main, to step Merge: 003120
- to stream Main, to step Curation: 003063
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Intersection Type Systems and Explicit Substitutions Calculi</title><author><name sortKey="Ventura, Daniel Lima" sort="Ventura, Daniel Lima" uniqKey="Ventura D" first="Daniel Lima" last="Ventura">Daniel Lima Ventura</name></author><author><name sortKey="Ayala Rinc N, Mauricio" sort="Ayala Rinc N, Mauricio" uniqKey="Ayala Rinc N M" first="Mauricio" last="Ayala-Rinc N">Mauricio Ayala-Rinc N</name></author><author><name sortKey="Kamareddine, Fairouz" sort="Kamareddine, Fairouz" uniqKey="Kamareddine F" first="Fairouz" last="Kamareddine">Fairouz Kamareddine</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:26E13A31AAB1A1D0A8EF435720F17E6E2CDAA20D</idno><date when="2010" year="2010">2010</date><idno type="doi">10.1007/978-3-642-13824-9_19</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-RZ7N8J1J-2/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000883</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000883</idno><idno type="wicri:Area/Istex/Curation">000878</idno><idno type="wicri:Area/Istex/Checkpoint">000825</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000825</idno><idno type="wicri:doubleKey">0302-9743:2010:Ventura D:intersection:type:systems</idno><idno type="wicri:Area/Main/Merge">003120</idno><idno type="wicri:Area/Main/Curation">003063</idno><idno type="wicri:Area/Main/Exploration">003063</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Intersection Type Systems and Explicit Substitutions Calculi</title><author><name sortKey="Ventura, Daniel Lima" sort="Ventura, Daniel Lima" uniqKey="Ventura D" first="Daniel Lima" last="Ventura">Daniel Lima Ventura</name><affiliation wicri:level="1"><country xml:lang="fr">Brésil</country><wicri:regionArea>Grupo de Teoria da Computação, Dep. de Matemática Universidade de Brasília, Brasília D.F.</wicri:regionArea><wicri:noRegion>Brasília D.F.</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Brésil</country></affiliation></author><author><name sortKey="Ayala Rinc N, Mauricio" sort="Ayala Rinc N, Mauricio" uniqKey="Ayala Rinc N M" first="Mauricio" last="Ayala-Rinc N">Mauricio Ayala-Rinc N</name><affiliation wicri:level="1"><country xml:lang="fr">Brésil</country><wicri:regionArea>Grupo de Teoria da Computação, Dep. de Matemática Universidade de Brasília, Brasília D.F.</wicri:regionArea><wicri:noRegion>Brasília D.F.</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Brésil</country></affiliation></author><author><name sortKey="Kamareddine, Fairouz" sort="Kamareddine, Fairouz" uniqKey="Kamareddine F" first="Fairouz" last="Kamareddine">Fairouz Kamareddine</name><affiliation wicri:level="3"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh</wicri:regionArea><placeName><settlement type="city">Édimbourg</settlement><region type="country">Écosse</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></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: The λ-calculus with de Bruijn indices, called λ dB , assembles each α-class of λ-terms into a unique term, using indices instead of variable names. Intersection types provide finitary type polymorphism satisfying important properties like principal typing, which allows the type system to include features such as data abstraction (modularity) and separate compilation. To be closer to computation and to simplify the formalisation of the atomic operations involved in β-contractions, several explicit substitution calculi were developed most of which are written with de Bruijn indices. Although untyped and simply types versions of explicit substitution calculi are well investigated, versions with more elaborate type systems (e.g., with intersection types) are not. In previous work, we presented a version for λ dB of an intersection type system originally introduced to characterise principal typings for β-normal forms and provided the characterisation for this version. In this work we introduce intersection type systems for two explicit substitution calculi: the λσ and the λs e . These type system are based on a type system for λ dB and satisfy the basic property of subject reduction, which guarantees the preservation of types during computations.</div></front></TEI><affiliations><list><country><li>Brésil</li><li>Royaume-Uni</li></country><region><li>Écosse</li></region><settlement><li>Édimbourg</li></settlement></list><tree><country name="Brésil"><noRegion><name sortKey="Ventura, Daniel Lima" sort="Ventura, Daniel Lima" uniqKey="Ventura D" first="Daniel Lima" last="Ventura">Daniel Lima Ventura</name></noRegion><name sortKey="Ayala Rinc N, Mauricio" sort="Ayala Rinc N, Mauricio" uniqKey="Ayala Rinc N M" first="Mauricio" last="Ayala-Rinc N">Mauricio Ayala-Rinc N</name><name sortKey="Ayala Rinc N, Mauricio" sort="Ayala Rinc N, Mauricio" uniqKey="Ayala Rinc N M" first="Mauricio" last="Ayala-Rinc N">Mauricio Ayala-Rinc N</name><name sortKey="Ventura, Daniel Lima" sort="Ventura, Daniel Lima" uniqKey="Ventura D" first="Daniel Lima" last="Ventura">Daniel Lima Ventura</name></country><country name="Royaume-Uni"><region name="Écosse"><name sortKey="Kamareddine, Fairouz" sort="Kamareddine, Fairouz" uniqKey="Kamareddine F" first="Fairouz" last="Kamareddine">Fairouz Kamareddine</name></region><name sortKey="Kamareddine, Fairouz" sort="Kamareddine, Fairouz" uniqKey="Kamareddine F" first="Fairouz" last="Kamareddine">Fairouz Kamareddine</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003063 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003063 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:26E13A31AAB1A1D0A8EF435720F17E6E2CDAA20D
|texte= Intersection Type Systems and Explicit Substitutions Calculi
}}
| This area was generated with Dilib version V0.6.33. |  |