Realizability models for BLL-like languages
Identifieur interne : 007011 ( Main/Merge ); précédent : 007010; suivant : 007012Realizability models for BLL-like languages
Auteurs : M. Hofmann [Allemagne] ; P. J. Scott [Canada]Source :
- Theoretical computer science [ 0304-3975 ] ; 2004.
Descripteurs français
- Pascal (Inist)
English descriptors
Abstract
jjkWe give a realizability model of Girard-Scedrov-Scott's Bounded Linear Logic (BLL). This gives a new proof that all numerical functions representable in that system are polytime. Our analysis naturally justifies the design of the BLL syntax and suggests further extensions.
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000661
- to stream PascalFrancis, to step Curation: 000380
- to stream PascalFrancis, to step Checkpoint: 000576
Links to Exploration step
Pascal:04-0318320Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Realizability models for BLL-like languages</title><author><name sortKey="Hofmann, M" sort="Hofmann, M" uniqKey="Hofmann M" first="M." last="Hofmann">M. Hofmann</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>Institut für Informatik, Ludwig-Maximilians-Universität München, Oettingenstrasse 67</s1><s2>80538, München</s2><s3>DEU</s3><sZ>1 aut.</sZ></inist:fA14><country>Allemagne</country><placeName><region type="land" nuts="1">Bavière</region><region type="district" nuts="2">District de Haute-Bavière</region><settlement type="city">Munich</settlement></placeName><orgName type="university">Université Louis-et-Maximilien de Munich</orgName></affiliation></author><author><name sortKey="Scott, P J" sort="Scott, P J" uniqKey="Scott P" first="P. J." last="Scott">P. J. Scott</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Department of Mathematics & Statistics, University of Ottawa, 585 King Edward</s1><s2>Ottawa Ont., K1N6N5</s2><s3>CAN</s3><sZ>2 aut.</sZ></inist:fA14><country>Canada</country><wicri:noRegion>Ottawa Ont., K1N6N5</wicri:noRegion></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">04-0318320</idno><date when="2004">2004</date><idno type="stanalyst">PASCAL 04-0318320 INIST</idno><idno type="RBID">Pascal:04-0318320</idno><idno type="wicri:Area/PascalFrancis/Corpus">000661</idno><idno type="wicri:Area/PascalFrancis/Curation">000380</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000576</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000576</idno><idno type="wicri:doubleKey">0304-3975:2004:Hofmann M:realizability:models:for</idno><idno type="wicri:Area/Main/Merge">007011</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Realizability models for BLL-like languages</title><author><name sortKey="Hofmann, M" sort="Hofmann, M" uniqKey="Hofmann M" first="M." last="Hofmann">M. Hofmann</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>Institut für Informatik, Ludwig-Maximilians-Universität München, Oettingenstrasse 67</s1><s2>80538, München</s2><s3>DEU</s3><sZ>1 aut.</sZ></inist:fA14><country>Allemagne</country><placeName><region type="land" nuts="1">Bavière</region><region type="district" nuts="2">District de Haute-Bavière</region><settlement type="city">Munich</settlement></placeName><orgName type="university">Université Louis-et-Maximilien de Munich</orgName></affiliation></author><author><name sortKey="Scott, P J" sort="Scott, P J" uniqKey="Scott P" first="P. J." last="Scott">P. J. Scott</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Department of Mathematics & Statistics, University of Ottawa, 585 King Edward</s1><s2>Ottawa Ont., K1N6N5</s2><s3>CAN</s3><sZ>2 aut.</sZ></inist:fA14><country>Canada</country><wicri:noRegion>Ottawa Ont., K1N6N5</wicri:noRegion></affiliation></author></analytic><series><title level="j" type="main">Theoretical computer science</title><title level="j" type="abbreviated">Theor. comput. sci.</title><idno type="ISSN">0304-3975</idno><imprint><date when="2004">2004</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Theoretical computer science</title><title level="j" type="abbreviated">Theor. comput. sci.</title><idno type="ISSN">0304-3975</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Bounded linear logic</term><term>Computer theory</term><term>Realization theory</term><term>Syntax</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Théorie réalisation</term><term>Syntaxe</term><term>Informatique théorique</term><term>05Bxx</term><term>Logique linéaire bornée</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">jjkWe give a realizability model of Girard-Scedrov-Scott's Bounded Linear Logic (BLL). This gives a new proof that all numerical functions representable in that system are polytime. Our analysis naturally justifies the design of the BLL syntax and suggests further extensions.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>Canada</li></country><region><li>Bavière</li><li>District de Haute-Bavière</li></region><settlement><li>Munich</li></settlement><orgName><li>Université Louis-et-Maximilien de Munich</li></orgName></list><tree><country name="Allemagne"><region name="Bavière"><name sortKey="Hofmann, M" sort="Hofmann, M" uniqKey="Hofmann M" first="M." last="Hofmann">M. Hofmann</name></region></country><country name="Canada"><noRegion><name sortKey="Scott, P J" sort="Scott, P J" uniqKey="Scott P" first="P. J." last="Scott">P. J. Scott</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 007011 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 007011 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= Pascal:04-0318320
|texte= Realizability models for BLL-like languages
}}
| This area was generated with Dilib version V0.6.33. |  |