Perpetuality for Full and Safe Composition (in a Constructive Setting)
Identifieur interne : 003274 ( Istex/Corpus ); précédent : 003273; suivant : 003275Perpetuality for Full and Safe Composition (in a Constructive Setting)
Auteurs : Delia KesnerSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We study perpetuality in calculi with explicit substitutions having full composition. A simple perpetual strategy is used to define strongly normalising terms inductively. This gives a simple argument to show preservation of β-strong normalisation as well as strong normalisation for typed terms. Particularly, the strong normalisation proof is based on implicit substitution rather than explicit substitution, so that it turns out to be modular w.r.t. the well-known proofs for typed lambda-calculus. All the proofs we develop are constructive.
Url:
DOI: 10.1007/978-3-540-70583-3_26
Links to Exploration step
ISTEX:D4EDEFC62BFF2A4FA03B0AAFB5D3D636B9789AF8Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Perpetuality for Full and Safe Composition (in a Constructive Setting)</title><author><name sortKey="Kesner, Delia" sort="Kesner, Delia" uniqKey="Kesner D" first="Delia" last="Kesner">Delia Kesner</name><affiliation><mods:affiliation>PPS, Université Paris Diderot, </mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:D4EDEFC62BFF2A4FA03B0AAFB5D3D636B9789AF8</idno><date when="2008" year="2008">2008</date><idno type="doi">10.1007/978-3-540-70583-3_26</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-MQ9X8865-C/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003274</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003274</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Perpetuality for Full and Safe Composition (in a Constructive Setting)</title><author><name sortKey="Kesner, Delia" sort="Kesner, Delia" uniqKey="Kesner D" first="Delia" last="Kesner">Delia Kesner</name><affiliation><mods:affiliation>PPS, Université Paris Diderot, </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: We study perpetuality in calculi with explicit substitutions having full composition. A simple perpetual strategy is used to define strongly normalising terms inductively. This gives a simple argument to show preservation of β-strong normalisation as well as strong normalisation for typed terms. Particularly, the strong normalisation proof is based on implicit substitution rather than explicit substitution, so that it turns out to be modular w.r.t. the well-known proofs for typed lambda-calculus. All the proofs we develop are constructive.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Delia Kesner</name><affiliations><json:string>PPS, Université Paris Diderot,</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-MQ9X8865-C</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>proceedings</json:string></originalGenre><abstract>Abstract: We study perpetuality in calculi with explicit substitutions having full composition. A simple perpetual strategy is used to define strongly normalising terms inductively. This gives a simple argument to show preservation of β-strong normalisation as well as strong normalisation for typed terms. Particularly, the strong normalisation proof is based on implicit substitution rather than explicit substitution, so that it turns out to be modular w.r.t. the well-known proofs for typed lambda-calculus. All the proofs we develop are constructive.</abstract><qualityIndicators><refBibsNative>false</refBibsNative><abstractWordCount>79</abstractWordCount><abstractCharCount>555</abstractCharCount><keywordCount>0</keywordCount><score>7.948</score><pdfWordCount>5196</pdfWordCount><pdfCharCount>26335</pdfCharCount><pdfVersion>1.6</pdfVersion><pdfPageCount>12</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize></qualityIndicators><title>Perpetuality for Full and Safe Composition (in a Constructive Setting)</title><chapterId><json:string>26</json:string><json:string>Chap26</json:string></chapterId><genre><json:string>conference</json:string></genre><serie><title>Lecture Notes in Computer Science</title><language><json:string>unknown</json:string></language><copyrightDate>2008</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>David Hutchison</name></json:item><json:item><name>Takeo Kanade</name></json:item><json:item><name>Josef Kittler</name></json:item><json:item><name>Jon M. Kleinberg</name></json:item><json:item><name>Friedemann Mattern</name></json:item><json:item><name>John C. Mitchell</name></json:item><json:item><name>Moni Naor</name></json:item><json:item><name>Oscar Nierstrasz</name></json:item><json:item><name>C. Pandu Rangan</name></json:item><json:item><name>Bernhard Steffen</name></json:item><json:item><name>Madhu Sudan</name></json:item><json:item><name>Demetri Terzopoulos</name></json:item><json:item><name>Doug Tygar</name></json:item><json:item><name>Moshe Y. Vardi</name></json:item><json:item><name>Gerhard Weikum</name></json:item></editor></serie><host><title>Automata, Languages and Programming</title><language><json:string>unknown</json:string></language><copyrightDate>2008</copyrightDate><doi><json:string>10.1007/978-3-540-70583-3</json:string></doi><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><eisbn><json:string>978-3-540-70583-3</json:string></eisbn><bookId><json:string>978-3-540-70583-3</json:string></bookId><isbn><json:string>978-3-540-70582-6</json:string></isbn><volume>5126</volume><pages><first>311</first><last>322</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Luca Aceto</name></json:item><json:item><name>Ivan Damgård</name></json:item><json:item><name>Leslie Ann Goldberg</name></json:item><json:item><name>Magnús M. Halldórsson</name></json:item><json:item><name>Anna Ingólfsdóttir</name></json:item><json:item><name>Igor Walukiewicz</name></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Theory of Computation</value></json:item><json:item><value>Software Engineering/Programming and Operating Systems</value></json:item><json:item><value>Discrete Mathematics in Computer Science</value></json:item><json:item><value>Numeric Computing</value></json:item><json:item><value>Data Structures</value></json:item><json:item><value>Data Structures, Cryptology and Information Theory</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-MQ9X8865-C</json:string></ark><publicationDate>2008</publicationDate><copyrightDate>2008</copyrightDate><doi><json:string>10.1007/978-3-540-70583-3_26</json:string></doi><id>D4EDEFC62BFF2A4FA03B0AAFB5D3D636B9789AF8</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-MQ9X8865-C/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-MQ9X8865-C/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-MQ9X8865-C/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Perpetuality for Full and Safe Composition (in a Constructive Setting)</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2008">2008</date></publicationStmt><notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note><note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note></notesStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Perpetuality for Full and Safe Composition (in a Constructive Setting)</title><author><persName><forename type="first">Delia</forename><surname>Kesner</surname></persName><affiliation><orgName type="department">PPS</orgName><orgName type="institution">Université Paris Diderot</orgName><address><country key=""></country></address></affiliation></author><idno type="istex">D4EDEFC62BFF2A4FA03B0AAFB5D3D636B9789AF8</idno><idno type="ark">ark:/67375/HCB-MQ9X8865-C</idno><idno type="DOI">10.1007/978-3-540-70583-3_26</idno></analytic><monogr><title level="m" type="main">Automata, Languages and Programming</title><title level="m" type="sub">35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II</title><title level="m" type="part">Track B: Logic, Semantics, and Theory of Programming</title><idno type="DOI">10.1007/978-3-540-70583-3</idno><idno type="book-id">978-3-540-70583-3</idno><idno type="ISBN">978-3-540-70582-6</idno><idno type="eISBN">978-3-540-70583-3</idno><idno type="chapter-id">Chap26</idno><idno type="part-id">Part2</idno><editor><persName><forename type="first">Luca</forename><surname>Aceto</surname></persName><email>luca@ru.is</email></editor><editor><persName><forename type="first">Ivan</forename><surname>Damgård</surname></persName><email>ivan@daimi.au.dk</email></editor><editor><persName><forename type="first">Leslie</forename><forename type="first">Ann</forename><surname>Goldberg</surname></persName><email>l.a.leslie@liverpool.uk</email></editor><editor><persName><forename type="first">Magnús</forename><forename type="first">M.</forename><surname>Halldórsson</surname></persName><email>mmh@ru.is</email></editor><editor><persName><forename type="first">Anna</forename><surname>Ingólfsdóttir</surname></persName><email>annai@ru.is</email></editor><editor><persName><forename type="first">Igor</forename><surname>Walukiewicz</surname></persName><email>igw@labri.fr</email></editor><imprint><biblScope unit="vol">5126</biblScope><biblScope unit="page" from="311">311</biblScope><biblScope unit="page" to="322">322</biblScope><biblScope unit="chapter-count">58</biblScope><biblScope unit="part-chapter-count">32</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><editor><persName><forename type="first">David</forename><surname>Hutchison</surname></persName></editor><editor><persName><forename type="first">Takeo</forename><surname>Kanade</surname></persName></editor><editor><persName><forename type="first">Josef</forename><surname>Kittler</surname></persName></editor><editor><persName><forename type="first">Jon</forename><forename type="first">M.</forename><surname>Kleinberg</surname></persName></editor><editor><persName><forename type="first">Friedemann</forename><surname>Mattern</surname></persName></editor><editor><persName><forename type="first">John</forename><forename type="first">C.</forename><surname>Mitchell</surname></persName></editor><editor><persName><forename type="first">Moni</forename><surname>Naor</surname></persName></editor><editor><persName><forename type="first">Oscar</forename><surname>Nierstrasz</surname></persName></editor><editor><persName><forename type="first">C.</forename><surname>Pandu Rangan</surname></persName></editor><editor><persName><forename type="first">Bernhard</forename><surname>Steffen</surname></persName></editor><editor><persName><forename type="first">Madhu</forename><surname>Sudan</surname></persName></editor><editor><persName><forename type="first">Demetri</forename><surname>Terzopoulos</surname></persName></editor><editor><persName><forename type="first">Doug</forename><surname>Tygar</surname></persName></editor><editor><persName><forename type="first">Moshe</forename><forename type="first">Y.</forename><surname>Vardi</surname></persName></editor><editor><persName><forename type="first">Gerhard</forename><surname>Weikum</surname></persName></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>We study perpetuality in calculi with explicit substitutions having <hi rend="italic">full composition</hi>. A simple perpetual strategy is used to define strongly normalising terms inductively. This gives a simple argument to show preservation of <hi rend="italic">β</hi>-strong normalisation as well as strong normalisation for typed terms. Particularly, the strong normalisation proof is based on implicit substitution rather than explicit substitution, so that it turns out to be modular w.r.t. the well-known proofs for typed lambda-calculus. All the proofs we develop are constructive.</p></abstract><textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject"><list><label>I</label><item><term type="Primary">Computer Science</term></item><label>I16005</label><item><term type="Secondary" subtype="priority-1">Theory of Computation</term></item><label>I14002</label><item><term type="Secondary" subtype="priority-2">Software Engineering/Programming and Operating Systems</term></item><label>I17028</label><item><term type="Secondary" subtype="priority-3">Discrete Mathematics in Computer Science</term></item><label>I1701X</label><item><term type="Secondary" subtype="priority-4">Numeric Computing</term></item><label>I15017</label><item><term type="Secondary" subtype="priority-5">Data Structures</term></item><label>I15009</label><item><term type="Secondary" subtype="priority-6">Data Structures, Cryptology and Information Theory</term></item></list></keywords></textClass><langUsage><language ident="EN"></language></langUsage></profileDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-MQ9X8865-C/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-ebooks not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>David</GivenName><FamilyName>Hutchison</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName><FamilyName>Kanade</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName><FamilyName>Kittler</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName><GivenName>M.</GivenName><FamilyName>Kleinberg</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName><FamilyName>Mattern</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>John</GivenName><GivenName>C.</GivenName><FamilyName>Mitchell</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName><FamilyName>Naor</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName><FamilyName>Nierstrasz</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>C.</GivenName><FamilyName>Pandu Rangan</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName><FamilyName>Steffen</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName><FamilyName>Sudan</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName><FamilyName>Terzopoulos</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Doug</GivenName><FamilyName>Tygar</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName><GivenName>Y.</GivenName><FamilyName>Vardi</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Weikum</FamilyName></EditorName></Editor></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" OutputMedium="All" TocLevels="0"><BookID>978-3-540-70583-3</BookID><BookTitle>Automata, Languages and Programming</BookTitle><BookSubTitle>35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II</BookSubTitle><BookVolumeNumber>5126</BookVolumeNumber><BookSequenceNumber>5126</BookSequenceNumber><BookDOI>10.1007/978-3-540-70583-3</BookDOI><BookTitleID>164832</BookTitleID><BookPrintISBN>978-3-540-70582-6</BookPrintISBN><BookElectronicISBN>978-3-540-70583-3</BookElectronicISBN><BookChapterCount>58</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2008</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I16005" Priority="1" Type="Secondary">Theory of Computation</BookSubject><BookSubject Code="I14002" Priority="2" Type="Secondary">Software Engineering/Programming and Operating Systems</BookSubject><BookSubject Code="I17028" Priority="3" Type="Secondary">Discrete Mathematics in Computer Science</BookSubject><BookSubject Code="I1701X" Priority="4" Type="Secondary">Numeric Computing</BookSubject><BookSubject Code="I15017" Priority="5" Type="Secondary">Data Structures</BookSubject><BookSubject Code="I15009" Priority="6" Type="Secondary">Data Structures, Cryptology and Information Theory</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup></BookInfo><BookHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Luca</GivenName><FamilyName>Aceto</FamilyName></EditorName><Contact><Email>luca@ru.is</Email></Contact></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Ivan</GivenName><FamilyName>Damgård</FamilyName></EditorName><Contact><Email>ivan@daimi.au.dk</Email></Contact></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Leslie</GivenName><GivenName>Ann</GivenName><FamilyName>Goldberg</FamilyName></EditorName><Contact><Email>l.a.leslie@liverpool.uk</Email></Contact></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Magnús</GivenName><GivenName>M.</GivenName><FamilyName>Halldórsson</FamilyName></EditorName><Contact><Email>mmh@ru.is</Email></Contact></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Anna</GivenName><FamilyName>Ingólfsdóttir</FamilyName></EditorName><Contact><Email>annai@ru.is</Email></Contact></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Igor</GivenName><FamilyName>Walukiewicz</FamilyName></EditorName><Contact><Email>igw@labri.fr</Email></Contact></Editor></EditorGroup></BookHeader><Part ID="Part2"><PartInfo TocLevels="0"><PartID>2</PartID><PartSequenceNumber>2</PartSequenceNumber><PartTitle>Track B: Logic, Semantics, and Theory of Programming</PartTitle><PartChapterCount>32</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Automata, Languages and Programming</BookTitle></PartContext></PartInfo><SubPart ID="SubPart7"><SubPartInfo><SubPartID>7</SubPartID><SubPartSequenceNumber>7</SubPartSequenceNumber><SubPartTitle>Reasoning about Computation</SubPartTitle><SubPartChapterCount>4</SubPartChapterCount></SubPartInfo><Chapter ID="Chap26" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>26</ChapterID><ChapterDOI>10.1007/978-3-540-70583-3_26</ChapterDOI><ChapterSequenceNumber>26</ChapterSequenceNumber><ChapterTitle Language="En">Perpetuality for Full and Safe Composition (in a Constructive Setting)</ChapterTitle><ChapterFirstPage>311</ChapterFirstPage><ChapterLastPage>322</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2008</CopyrightYear></ChapterCopyright><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><PartID>2</PartID><BookID>978-3-540-70583-3</BookID><BookTitle>Automata, Languages and Programming</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Delia</GivenName><FamilyName>Kesner</FamilyName></AuthorName></Author><Affiliation ID="Aff1"><OrgDivision>PPS</OrgDivision><OrgName>Université Paris Diderot</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>We study perpetuality in calculi with explicit substitutions having <Emphasis Type="Italic">full composition</Emphasis>. A simple perpetual strategy is used to define strongly normalising terms inductively. This gives a simple argument to show preservation of <Emphasis Type="Italic">β</Emphasis>-strong normalisation as well as strong normalisation for typed terms. Particularly, the strong normalisation proof is based on implicit substitution rather than explicit substitution, so that it turns out to be modular w.r.t. the well-known proofs for typed lambda-calculus. All the proofs we develop are constructive.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></SubPart></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Perpetuality for Full and Safe Composition (in a Constructive Setting)</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Perpetuality for Full and Safe Composition (in a Constructive Setting)</title></titleInfo><name type="personal"><namePart type="given">Delia</namePart><namePart type="family">Kesner</namePart><affiliation>PPS, Université Paris Diderot, </affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="conference" displayLabel="proceedings" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3"></genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2008</dateIssued><copyrightDate encoding="w3cdtf">2008</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: We study perpetuality in calculi with explicit substitutions having full composition. A simple perpetual strategy is used to define strongly normalising terms inductively. This gives a simple argument to show preservation of β-strong normalisation as well as strong normalisation for typed terms. Particularly, the strong normalisation proof is based on implicit substitution rather than explicit substitution, so that it turns out to be modular w.r.t. the well-known proofs for typed lambda-calculus. All the proofs we develop are constructive.</abstract><relatedItem type="host"><titleInfo><title>Automata, Languages and Programming</title><subTitle>35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II</subTitle></titleInfo><name type="personal"><namePart type="given">Luca</namePart><namePart type="family">Aceto</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Ivan</namePart><namePart type="family">Damgård</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Leslie</namePart><namePart type="given">Ann</namePart><namePart type="family">Goldberg</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Magnús</namePart><namePart type="given">M.</namePart><namePart type="family">Halldórsson</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Anna</namePart><namePart type="family">Ingólfsdóttir</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Igor</namePart><namePart type="family">Walukiewicz</namePart><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2008</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I16005">Theory of Computation</topic><topic authority="SpringerSubjectCodes" authorityURI="I14002">Software Engineering/Programming and Operating Systems</topic><topic authority="SpringerSubjectCodes" authorityURI="I17028">Discrete Mathematics in Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I1701X">Numeric Computing</topic><topic authority="SpringerSubjectCodes" authorityURI="I15017">Data Structures</topic><topic authority="SpringerSubjectCodes" authorityURI="I15009">Data Structures, Cryptology and Information Theory</topic></subject><identifier type="DOI">10.1007/978-3-540-70583-3</identifier><identifier type="ISBN">978-3-540-70582-6</identifier><identifier type="eISBN">978-3-540-70583-3</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">164832</identifier><identifier type="BookID">978-3-540-70583-3</identifier><identifier type="BookChapterCount">58</identifier><identifier type="BookVolumeNumber">5126</identifier><identifier type="BookSequenceNumber">5126</identifier><identifier type="PartChapterCount">32</identifier><part><date>2008</date><detail type="part"><title>Track B: Logic, Semantics, and Theory of Programming</title></detail><detail type="volume"><number>5126</number><caption>vol.</caption></detail><extent unit="pages"><start>311</start><end>322</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2008</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon</namePart><namePart type="given">M.</namePart><namePart type="family">Kleinberg</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John</namePart><namePart type="given">C.</namePart><namePart type="family">Mitchell</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Doug</namePart><namePart type="family">Tygar</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe</namePart><namePart type="given">Y.</namePart><namePart type="family">Vardi</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2008</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2008</recordOrigin></recordInfo></relatedItem><identifier type="istex">D4EDEFC62BFF2A4FA03B0AAFB5D3D636B9789AF8</identifier><identifier type="ark">ark:/67375/HCB-MQ9X8865-C</identifier><identifier type="DOI">10.1007/978-3-540-70583-3_26</identifier><identifier type="ChapterID">26</identifier><identifier type="ChapterID">Chap26</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2008</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2008</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-MQ9X8865-C/record.json</uri></json:item></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003274 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 003274 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:D4EDEFC62BFF2A4FA03B0AAFB5D3D636B9789AF8
|texte= Perpetuality for Full and Safe Composition (in a Constructive Setting)
}}
| This area was generated with Dilib version V0.6.33. |  |