The Prismoid of Resources
Identifieur interne : 003C27 ( Istex/Corpus ); précédent : 003C26; suivant : 003C28The Prismoid of Resources
Auteurs : Delia Kesner ; Fabien RenaudSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We define a framework called the prismoid of resources where each vertex refines the λ-calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of β-reduction, confluence, preservation of β-strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter, so that the properties for each vertex are obtained as a particular case of the general abstract proofs.
Url:
DOI: 10.1007/978-3-642-03816-7_40
Links to Exploration step
ISTEX:FB5AB42BA96766F51065DA8210F22C7A06391B60Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">The Prismoid of Resources</title><author><name sortKey="Kesner, Delia" sort="Kesner, Delia" uniqKey="Kesner D" first="Delia" last="Kesner">Delia Kesner</name><affiliation><mods:affiliation>PPS, CNRS and Université Paris Diderot, </mods:affiliation></affiliation></author><author><name sortKey="Renaud, Fabien" sort="Renaud, Fabien" uniqKey="Renaud F" first="Fabien" last="Renaud">Fabien Renaud</name><affiliation><mods:affiliation>PPS, CNRS and Université Paris Diderot, </mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FB5AB42BA96766F51065DA8210F22C7A06391B60</idno><date when="2009" year="2009">2009</date><idno type="doi">10.1007/978-3-642-03816-7_40</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-D7755Q7Z-V/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003C27</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003C27</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">The Prismoid of Resources</title><author><name sortKey="Kesner, Delia" sort="Kesner, Delia" uniqKey="Kesner D" first="Delia" last="Kesner">Delia Kesner</name><affiliation><mods:affiliation>PPS, CNRS and Université Paris Diderot, </mods:affiliation></affiliation></author><author><name sortKey="Renaud, Fabien" sort="Renaud, Fabien" uniqKey="Renaud F" first="Fabien" last="Renaud">Fabien Renaud</name><affiliation><mods:affiliation>PPS, CNRS and 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 define a framework called the prismoid of resources where each vertex refines the λ-calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of β-reduction, confluence, preservation of β-strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter, so that the properties for each vertex are obtained as a particular case of the general abstract proofs.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Delia Kesner</name><affiliations><json:string>PPS, CNRS and Université Paris Diderot,</json:string></affiliations></json:item><json:item><name>Fabien Renaud</name><affiliations><json:string>PPS, CNRS and Université Paris Diderot,</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-D7755Q7Z-V</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: We define a framework called the prismoid of resources where each vertex refines the λ-calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of β-reduction, confluence, preservation of β-strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter, so that the properties for each vertex are obtained as a particular case of the general abstract proofs.</abstract><qualityIndicators><score>8.284</score><pdfWordCount>5342</pdfWordCount><pdfCharCount>25155</pdfCharCount><pdfVersion>1.6</pdfVersion><pdfPageCount>13</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>107</abstractWordCount><abstractCharCount>706</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>The Prismoid of Resources</title><chapterId><json:string>40</json:string><json:string>Chap40</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>2009</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>David Hutchison</name><affiliations><json:string>Lancaster University, Lancaster, UK</json:string></affiliations></json:item><json:item><name>Takeo Kanade</name><affiliations><json:string>Carnegie Mellon University, Pittsburgh, PA, USA</json:string></affiliations></json:item><json:item><name>Josef Kittler</name><affiliations><json:string>University of Surrey, Guildford, UK</json:string></affiliations></json:item><json:item><name>Jon M. Kleinberg</name><affiliations><json:string>Cornell University, Ithaca, NY, USA</json:string></affiliations></json:item><json:item><name>Friedemann Mattern</name><affiliations><json:string>ETH Zurich, Zurich, Switzerland</json:string></affiliations></json:item><json:item><name>John C. Mitchell</name><affiliations><json:string>Stanford University, Stanford, CA, USA</json:string></affiliations></json:item><json:item><name>Moni Naor</name><affiliations><json:string>Weizmann Institute of Science, Rehovot, Israel</json:string></affiliations></json:item><json:item><name>Oscar Nierstrasz</name><affiliations><json:string>University of Bern, Bern, Switzerland</json:string></affiliations></json:item><json:item><name>C. Pandu Rangan</name><affiliations><json:string>Indian Institute of Technology, Madras, India</json:string></affiliations></json:item><json:item><name>Bernhard Steffen</name><affiliations><json:string>University of Dortmund, Dortmund, Germany</json:string></affiliations></json:item><json:item><name>Madhu Sudan</name><affiliations><json:string>Massachusetts Institute of Technology, MA, USA</json:string></affiliations></json:item><json:item><name>Demetri Terzopoulos</name><affiliations><json:string>University of California, Los Angeles, CA, USA</json:string></affiliations></json:item><json:item><name>Doug Tygar</name><affiliations><json:string>University of California, Berkeley, CA, USA</json:string></affiliations></json:item><json:item><name>Moshe Y. Vardi</name><affiliations><json:string>Rice University, Houston, TX, USA</json:string></affiliations></json:item><json:item><name>Gerhard Weikum</name><affiliations><json:string>Max-Planck Institute of Computer Science, Saarbrücken, Germany</json:string></affiliations></json:item></editor></serie><host><title>Mathematical Foundations of Computer Science 2009</title><language><json:string>unknown</json:string></language><copyrightDate>2009</copyrightDate><doi><json:string>10.1007/978-3-642-03816-7</json:string></doi><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><eisbn><json:string>978-3-642-03816-7</json:string></eisbn><bookId><json:string>978-3-642-03816-7</json:string></bookId><isbn><json:string>978-3-642-03815-0</json:string></isbn><volume>5734</volume><pages><first>464</first><last>476</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Rastislav Královič</name><affiliations><json:string>Department of Computer Science, Faculty of Mathematics, Physics and Informatics, Comenius University, Research partially funded by grant APVV 0433-06, Bratislava, Slovakia</json:string><json:string>E-mail: kralovic@dcs.fmph.uniba.sk</json:string></affiliations></json:item><json:item><name>Damian Niwiński</name><affiliations><json:string>Members of EACSL Jury for the Ackermann Award,</json:string><json:string>E-mail: niwinski@mimuw.edu.pl</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Algorithm Analysis and Problem Complexity</value></json:item><json:item><value>Computation by Abstract Devices</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item><json:item><value>Mathematics of Computing</value></json:item><json:item><value>Data Structures</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-D7755Q7Z-V</json:string></ark><publicationDate>2009</publicationDate><copyrightDate>2009</copyrightDate><doi><json:string>10.1007/978-3-642-03816-7_40</json:string></doi><id>FB5AB42BA96766F51065DA8210F22C7A06391B60</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-D7755Q7Z-V/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-D7755Q7Z-V/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-D7755Q7Z-V/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">The Prismoid of Resources</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2009">2009</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">The Prismoid of Resources</title><author><persName><forename type="first">Delia</forename><surname>Kesner</surname></persName><affiliation><orgName type="institution">PPS, CNRS and Université Paris Diderot</orgName><address><country key=""></country></address></affiliation></author><author><persName><forename type="first">Fabien</forename><surname>Renaud</surname></persName><affiliation><orgName type="institution">PPS, CNRS and Université Paris Diderot</orgName><address><country key=""></country></address></affiliation></author><idno type="istex">FB5AB42BA96766F51065DA8210F22C7A06391B60</idno><idno type="ark">ark:/67375/HCB-D7755Q7Z-V</idno><idno type="DOI">10.1007/978-3-642-03816-7_40</idno></analytic><monogr><title level="m" type="main">Mathematical Foundations of Computer Science 2009</title><title level="m" type="sub">34th International Symposium, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009. Proceedings</title><title level="m" type="part">Contributed Papers</title><idno type="DOI">10.1007/978-3-642-03816-7</idno><idno type="book-id">978-3-642-03816-7</idno><idno type="ISBN">978-3-642-03815-0</idno><idno type="eISBN">978-3-642-03816-7</idno><idno type="chapter-id">Chap40</idno><idno type="part-id">Part2</idno><editor><persName><forename type="first">Rastislav</forename><surname>Královič</surname></persName><email>kralovic@dcs.fmph.uniba.sk</email><affiliation><orgName type="department">Department of Computer Science, Faculty of Mathematics, Physics and Informatics</orgName><orgName type="institution">Comenius University, Research partially funded by grant APVV 0433-06</orgName><address><settlement>Bratislava</settlement><country key="SK">SLOVAKIA</country></address></affiliation></editor><editor><persName><forename type="first">Damian</forename><surname>Niwiński</surname></persName><email>niwinski@mimuw.edu.pl</email><affiliation><orgName type="institution">Members of EACSL Jury for the Ackermann Award</orgName><address><country key=""></country></address></affiliation></editor><imprint><biblScope unit="vol">5734</biblScope><biblScope unit="page" from="464">464</biblScope><biblScope unit="page" to="476">476</biblScope><biblScope unit="chapter-count">63</biblScope><biblScope unit="part-chapter-count">56</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><affiliation><orgName type="institution">Lancaster University</orgName><address><settlement>Lancaster</settlement><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Takeo</forename><surname>Kanade</surname></persName><affiliation><orgName type="institution">Carnegie Mellon University</orgName><address><settlement>Pittsburgh</settlement><region>PA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Josef</forename><surname>Kittler</surname></persName><affiliation><orgName type="institution">University of Surrey</orgName><address><settlement>Guildford</settlement><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Jon</forename><forename type="first">M.</forename><surname>Kleinberg</surname></persName><affiliation><orgName type="institution">Cornell University</orgName><address><settlement>Ithaca</settlement><region>NY</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Friedemann</forename><surname>Mattern</surname></persName><affiliation><orgName type="institution">ETH Zurich</orgName><address><settlement>Zurich</settlement><country key="CH">SWITZERLAND</country></address></affiliation></editor><editor><persName><forename type="first">John</forename><forename type="first">C.</forename><surname>Mitchell</surname></persName><affiliation><orgName type="institution">Stanford University</orgName><address><settlement>Stanford</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Moni</forename><surname>Naor</surname></persName><affiliation><orgName type="institution">Weizmann Institute of Science</orgName><address><settlement>Rehovot</settlement><country key="IL">ISRAEL</country></address></affiliation></editor><editor><persName><forename type="first">Oscar</forename><surname>Nierstrasz</surname></persName><affiliation><orgName type="institution">University of Bern</orgName><address><settlement>Bern</settlement><country key="CH">SWITZERLAND</country></address></affiliation></editor><editor><persName><forename type="first">C.</forename><surname>Pandu Rangan</surname></persName><affiliation><orgName type="institution">Indian Institute of Technology</orgName><address><settlement>Madras</settlement><country key="IN">INDIA</country></address></affiliation></editor><editor><persName><forename type="first">Bernhard</forename><surname>Steffen</surname></persName><affiliation><orgName type="institution">University of Dortmund</orgName><address><settlement>Dortmund</settlement><country key="DE">GERMANY</country></address></affiliation></editor><editor><persName><forename type="first">Madhu</forename><surname>Sudan</surname></persName><affiliation><orgName type="institution">Massachusetts Institute of Technology</orgName><address><region>MA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Demetri</forename><surname>Terzopoulos</surname></persName><affiliation><orgName type="institution">University of California</orgName><address><settlement>Los Angeles</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Doug</forename><surname>Tygar</surname></persName><affiliation><orgName type="institution">University of California</orgName><address><settlement>Berkeley</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Moshe</forename><forename type="first">Y.</forename><surname>Vardi</surname></persName><affiliation><orgName type="institution">Rice University</orgName><address><settlement>Houston</settlement><region>TX</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Gerhard</forename><surname>Weikum</surname></persName><affiliation><orgName type="institution">Max-Planck Institute of Computer Science</orgName><address><settlement>Saarbrücken</settlement><country key="DE">GERMANY</country></address></affiliation></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 define a framework called the <hi rend="italic">prismoid of resources</hi> where each vertex refines the <hi rend="italic">λ</hi>-calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of <hi rend="italic">β</hi>-reduction, confluence, preservation of <hi rend="italic">β</hi>-strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter, so that the properties for each vertex are obtained as a particular case of the general abstract proofs.</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>I16021</label><item><term type="Secondary" subtype="priority-1">Algorithm Analysis and Problem Complexity</term></item><label>I16013</label><item><term type="Secondary" subtype="priority-2">Computation by Abstract Devices</term></item><label>I1603X</label><item><term type="Secondary" subtype="priority-3">Logics and Meanings of Programs</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-4">Mathematical Logic and Formal Languages</term></item><label>I17001</label><item><term type="Secondary" subtype="priority-5">Mathematics of Computing</term></item><label>I15017</label><item><term type="Secondary" subtype="priority-6">Data Structures</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-D7755Q7Z-V/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 AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>David</GivenName><FamilyName>Hutchison</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName><FamilyName>Kanade</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName><FamilyName>Kittler</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName><GivenName>M.</GivenName><FamilyName>Kleinberg</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName><FamilyName>Mattern</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>John</GivenName><GivenName>C.</GivenName><FamilyName>Mitchell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName><FamilyName>Naor</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName><FamilyName>Nierstrasz</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff9"><EditorName DisplayOrder="Western"><GivenName>C.</GivenName><FamilyName>Pandu Rangan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff10"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName><FamilyName>Steffen</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff11"><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName><FamilyName>Sudan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff12"><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName><FamilyName>Terzopoulos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff13"><EditorName DisplayOrder="Western"><GivenName>Doug</GivenName><FamilyName>Tygar</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff14"><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName><GivenName>Y.</GivenName><FamilyName>Vardi</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff15"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Weikum</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Lancaster University</OrgName><OrgAddress><City>Lancaster</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>University of Surrey</OrgName><OrgAddress><City>Guildford</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgName>Cornell University</OrgName><OrgAddress><City>Ithaca</City><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgName>ETH Zurich</OrgName><OrgAddress><City>Zurich</City><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgName>Stanford University</OrgName><OrgAddress><City>Stanford</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>Weizmann Institute of Science</OrgName><OrgAddress><City>Rehovot</City><Country>Israel</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgName>University of Bern</OrgName><OrgAddress><City>Bern</City><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff9"><OrgName>Indian Institute of Technology</OrgName><OrgAddress><City>Madras</City><Country>India</Country></OrgAddress></Affiliation><Affiliation ID="Aff10"><OrgName>University of Dortmund</OrgName><OrgAddress><City>Dortmund</City><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff11"><OrgName>Massachusetts Institute of Technology</OrgName><OrgAddress><State>MA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff12"><OrgName>University of California</OrgName><OrgAddress><City>Los Angeles</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff13"><OrgName>University of California</OrgName><OrgAddress><City>Berkeley</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff14"><OrgName>Rice University</OrgName><OrgAddress><City>Houston</City><State>TX</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff15"><OrgName>Max-Planck Institute of Computer Science</OrgName><OrgAddress><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" OutputMedium="All" TocLevels="0"><BookID>978-3-642-03816-7</BookID><BookTitle>Mathematical Foundations of Computer Science 2009</BookTitle><BookSubTitle>34th International Symposium, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009. Proceedings</BookSubTitle><BookVolumeNumber>5734</BookVolumeNumber><BookSequenceNumber>5734</BookSequenceNumber><BookDOI>10.1007/978-3-642-03816-7</BookDOI><BookTitleID>190889</BookTitleID><BookPrintISBN>978-3-642-03815-0</BookPrintISBN><BookElectronicISBN>978-3-642-03816-7</BookElectronicISBN><BookChapterCount>63</BookChapterCount><BookCopyright><CopyrightHolderName>Springer Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2009</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I16021" Priority="1" Type="Secondary">Algorithm Analysis and Problem Complexity</BookSubject><BookSubject Code="I16013" Priority="2" Type="Secondary">Computation by Abstract Devices</BookSubject><BookSubject Code="I1603X" Priority="3" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I16048" Priority="4" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I17001" Priority="5" Type="Secondary">Mathematics of Computing</BookSubject><BookSubject Code="I15017" Priority="6" Type="Secondary">Data Structures</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff16"><EditorName DisplayOrder="Western"><GivenName>Rastislav</GivenName><FamilyName>Královič</FamilyName></EditorName><Contact><Email>kralovic@dcs.fmph.uniba.sk</Email></Contact></Editor><Editor AffiliationIDS="Aff17"><EditorName DisplayOrder="Western"><GivenName>Damian</GivenName><FamilyName>Niwiński</FamilyName></EditorName><Contact><Email>niwinski@mimuw.edu.pl</Email></Contact></Editor><Affiliation ID="Aff16"><OrgDivision>Department of Computer Science, Faculty of Mathematics, Physics and Informatics</OrgDivision><OrgName>Comenius University, Research partially funded by grant APVV 0433-06</OrgName><OrgAddress><City>Bratislava</City><Country>Slovakia</Country></OrgAddress></Affiliation><Affiliation ID="Aff17"><OrgName>Members of EACSL Jury for the Ackermann Award</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part2"><PartInfo TocLevels="0"><PartID>2</PartID><PartSequenceNumber>2</PartSequenceNumber><PartTitle>Contributed Papers</PartTitle><PartChapterCount>56</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Mathematical Foundations of Computer Science 2009</BookTitle></PartContext></PartInfo><Chapter ID="Chap40" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>40</ChapterID><ChapterDOI>10.1007/978-3-642-03816-7_40</ChapterDOI><ChapterSequenceNumber>40</ChapterSequenceNumber><ChapterTitle Language="En">The Prismoid of Resources</ChapterTitle><ChapterFirstPage>464</ChapterFirstPage><ChapterLastPage>476</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2009</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-642-03816-7</BookID><BookTitle>Mathematical Foundations of Computer Science 2009</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff18"><AuthorName DisplayOrder="Western"><GivenName>Delia</GivenName><FamilyName>Kesner</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff18"><AuthorName DisplayOrder="Western"><GivenName>Fabien</GivenName><FamilyName>Renaud</FamilyName></AuthorName></Author><Affiliation ID="Aff18"><OrgName>PPS, CNRS and Université Paris Diderot</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>We define a framework called the <Emphasis Type="Italic">prismoid of resources</Emphasis> where each vertex refines the <Emphasis Type="Italic">λ</Emphasis>-calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of <Emphasis Type="Italic">β</Emphasis>-reduction, confluence, preservation of <Emphasis Type="Italic">β</Emphasis>-strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter, so that the properties for each vertex are obtained as a particular case of the general abstract proofs.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>The Prismoid of Resources</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>The Prismoid of Resources</title></titleInfo><name type="personal"><namePart type="given">Delia</namePart><namePart type="family">Kesner</namePart><affiliation>PPS, CNRS and Université Paris Diderot, </affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Fabien</namePart><namePart type="family">Renaud</namePart><affiliation>PPS, CNRS and Université Paris Diderot, </affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2009</dateIssued><copyrightDate encoding="w3cdtf">2009</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: We define a framework called the prismoid of resources where each vertex refines the λ-calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of β-reduction, confluence, preservation of β-strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter, so that the properties for each vertex are obtained as a particular case of the general abstract proofs.</abstract><relatedItem type="host"><titleInfo><title>Mathematical Foundations of Computer Science 2009</title><subTitle>34th International Symposium, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Rastislav</namePart><namePart type="family">Královič</namePart><affiliation>Department of Computer Science, Faculty of Mathematics, Physics and Informatics, Comenius University, Research partially funded by grant APVV 0433-06, Bratislava, Slovakia</affiliation><affiliation>E-mail: kralovic@dcs.fmph.uniba.sk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Damian</namePart><namePart type="family">Niwiński</namePart><affiliation>Members of EACSL Jury for the Ackermann Award, </affiliation><affiliation>E-mail: niwinski@mimuw.edu.pl</affiliation><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">2009</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="I16021">Algorithm Analysis and Problem Complexity</topic><topic authority="SpringerSubjectCodes" authorityURI="I16013">Computation by Abstract Devices</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="I17001">Mathematics of Computing</topic><topic authority="SpringerSubjectCodes" authorityURI="I15017">Data Structures</topic></subject><identifier type="DOI">10.1007/978-3-642-03816-7</identifier><identifier type="ISBN">978-3-642-03815-0</identifier><identifier type="eISBN">978-3-642-03816-7</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">190889</identifier><identifier type="BookID">978-3-642-03816-7</identifier><identifier type="BookChapterCount">63</identifier><identifier type="BookVolumeNumber">5734</identifier><identifier type="BookSequenceNumber">5734</identifier><identifier type="PartChapterCount">56</identifier><part><date>2009</date><detail type="part"><title>Contributed Papers</title></detail><detail type="volume"><number>5734</number><caption>vol.</caption></detail><extent unit="pages"><start>464</start><end>476</end></extent></part><recordInfo><recordOrigin>Springer Berlin Heidelberg, 2009</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><affiliation>Lancaster University, Lancaster, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><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><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Zurich, Switzerland</affiliation><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><affiliation>Stanford University, Stanford, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>University of California, Los Angeles, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Doug</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><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><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbrücken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2009</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 Berlin Heidelberg, 2009</recordOrigin></recordInfo></relatedItem><identifier type="istex">FB5AB42BA96766F51065DA8210F22C7A06391B60</identifier><identifier type="ark">ark:/67375/HCB-D7755Q7Z-V</identifier><identifier type="DOI">10.1007/978-3-642-03816-7_40</identifier><identifier type="ChapterID">40</identifier><identifier type="ChapterID">Chap40</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer Berlin Heidelberg, 2009</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, 2009</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-D7755Q7Z-V/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 003C27 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 003C27 | 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:FB5AB42BA96766F51065DA8210F22C7A06391B60
|texte= The Prismoid of Resources
}}
| This area was generated with Dilib version V0.6.33. |  |