Realizability models for BLL-like languages
Identifieur interne :
000380 ( PascalFrancis/Curation );
précédent :
000379;
suivant :
000381
Realizability models for BLL-like languages
Auteurs : M. Hofmann [
Allemagne] ;
P. J. Scott [
Canada]
Source :
-
Theoretical computer science [ 0304-3975 ] ; 2004.
RBID : Pascal:04-0318320
Descripteurs français
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.
| pA |
| A01 | 01 | 1 | | @0 0304-3975 |
|---|
| A02 | 01 | | | @0 TCSCDI |
|---|
| A03 | | 1 | | @0 Theor. comput. sci. |
|---|
| A05 | | | | @2 318 |
|---|
| A06 | | | | @2 1-2 |
|---|
| A08 | 01 | 1 | ENG | @1 Realizability models for BLL-like languages |
|---|
| A09 | 01 | 1 | ENG | @1 Implicit computational complexity |
|---|
| A11 | 01 | 1 | | @1 HOFMANN (M.) |
|---|
| A11 | 02 | 1 | | @1 SCOTT (P. J.) |
|---|
| A12 | 01 | 1 | | @1 MARION (Jean-Yves) @9 ed. |
|---|
| A14 | 01 | | | @1 Institut für Informatik, Ludwig-Maximilians-Universität München, Oettingenstrasse 67 @2 80538, München @3 DEU @Z 1 aut. |
|---|
| A14 | 02 | | | @1 Department of Mathematics & Statistics, University of Ottawa, 585 King Edward @2 Ottawa Ont., K1N6N5 @3 CAN @Z 2 aut. |
|---|
| A15 | 01 | | | @1 LORIA-INPL, Ecole Nationale Superieure des Mines de Nancy, BP 239 @2 Vandoeuvre-les-Nancy 54506 @3 FRA @Z 1 aut. |
|---|
| A20 | | | | @1 121-137 |
|---|
| A21 | | | | @1 2004 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A43 | 01 | | | @1 INIST @2 17243 @5 354000110408220060 |
|---|
| A44 | | | | @0 0000 @1 © 2004 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 16 ref. |
|---|
| A47 | 01 | 1 | | @0 04-0318320 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Theoretical computer science |
|---|
| A66 | 01 | | | @0 NLD |
|---|
| C01 | 01 | | ENG | @0 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. |
|---|
| C02 | 01 | X | | @0 001D02A08 |
|---|
| C02 | 02 | X | | @0 001A02B01B |
|---|
| C03 | 01 | 3 | FRE | @0 Théorie réalisation @5 18 |
|---|
| C03 | 01 | 3 | ENG | @0 Realization theory @5 18 |
|---|
| C03 | 02 | X | FRE | @0 Syntaxe @5 19 |
|---|
| C03 | 02 | X | ENG | @0 Syntax @5 19 |
|---|
| C03 | 02 | X | SPA | @0 Sintaxis @5 19 |
|---|
| C03 | 03 | X | FRE | @0 Informatique théorique @5 20 |
|---|
| C03 | 03 | X | ENG | @0 Computer theory @5 20 |
|---|
| C03 | 03 | X | SPA | @0 Informática teórica @5 20 |
|---|
| C03 | 04 | X | FRE | @0 05Bxx @4 INC @5 70 |
|---|
| C03 | 05 | X | FRE | @0 Logique linéaire bornée @4 CD @5 96 |
|---|
| C03 | 05 | X | ENG | @0 Bounded linear logic @4 CD @5 96 |
|---|
| N21 | | | | @1 187 |
|---|
| N44 | 01 | | | @1 OTO |
|---|
| N82 | | | | @1 OTO |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 ICC Workshop @3 Santa Barbara, CA USA @4 2000 |
|---|
|
|---|
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000661
Links to Exploration step
Pascal:04-0318320
Le 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="1"><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>
</affiliation><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>
</affiliation><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>
</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="1"><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>
</affiliation><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>
</affiliation><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><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><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><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><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0304-3975</s0>
</fA01><fA02 i1="01"><s0>TCSCDI</s0>
</fA02><fA03 i2="1"><s0>Theor. comput. sci.</s0>
</fA03><fA05><s2>318</s2>
</fA05><fA06><s2>1-2</s2>
</fA06><fA08 i1="01" i2="1" l="ENG"><s1>Realizability models for BLL-like languages</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>Implicit computational complexity</s1>
</fA09><fA11 i1="01" i2="1"><s1>HOFMANN (M.)</s1>
</fA11><fA11 i1="02" i2="1"><s1>SCOTT (P. J.)</s1>
</fA11><fA12 i1="01" i2="1"><s1>MARION (Jean-Yves)</s1>
<s9>ed.</s9>
</fA12><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>
</fA14><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>
</fA14><fA15 i1="01"><s1>LORIA-INPL, Ecole Nationale Superieure des Mines de Nancy, BP 239</s1>
<s2>Vandoeuvre-les-Nancy 54506</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA15><fA20><s1>121-137</s1>
</fA20><fA21><s1>2004</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA43 i1="01"><s1>INIST</s1>
<s2>17243</s2>
<s5>354000110408220060</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2004 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>16 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>04-0318320</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><fA64 i1="01" i2="1"><s0>Theoretical computer science</s0>
</fA64><fA66 i1="01"><s0>NLD</s0>
</fA66><fC01 i1="01" l="ENG"><s0>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.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02A08</s0>
</fC02><fC02 i1="02" i2="X"><s0>001A02B01B</s0>
</fC02><fC03 i1="01" i2="3" l="FRE"><s0>Théorie réalisation</s0>
<s5>18</s5>
</fC03><fC03 i1="01" i2="3" l="ENG"><s0>Realization theory</s0>
<s5>18</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Syntaxe</s0>
<s5>19</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Syntax</s0>
<s5>19</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Sintaxis</s0>
<s5>19</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Informatique théorique</s0>
<s5>20</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Computer theory</s0>
<s5>20</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Informática teórica</s0>
<s5>20</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>05Bxx</s0>
<s4>INC</s4>
<s5>70</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Logique linéaire bornée</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Bounded linear logic</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fN21><s1>187</s1>
</fN21><fN44 i1="01"><s1>OTO</s1>
</fN44><fN82><s1>OTO</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>ICC Workshop</s1>
<s3>Santa Barbara, CA USA</s3>
<s4>2000</s4>
</fA30>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000380 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Curation/biblio.hfd -nk 000380 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Curation
|type= RBID
|clé= Pascal:04-0318320
|texte= Realizability models for BLL-like languages
}}
| This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022 |  |
