PittsburghV1, France, Analysis, bibRecord, 000145

Refinement Types for Incremental Computational Complexity

Identifieur interne : 000145 ( France/Analysis ); précédent : 000144; suivant : 000146

Refinement Types for Incremental Computational Complexity

Auteurs : Ezgi Çiçek [France, Allemagne] ; Deepak Garg [France, Allemagne] ; Umut Acar [États-Unis]

Source :

RBID : Hal:hal-01245888

Abstract

With recent advances, programs can be compiled to efficiently respond to incremental input changes. However, there is no language level support for reasoning about the time complexity of incremental updates. Motivated by this gap, we present CostIt, a higher-order functional language with a lightweight refinement type system for proving asymptotic bounds on incremental computation time. Type refinements specify which parts of inputs and outputs may change, as well as dynamic stability, a measure of time required to propagate changes to a program's execution trace, given modified inputs. We prove our type system sound using a new step-indexed cost semantics for change propagation and demonstrate the precision and generality of our technique through examples.

Url:

https://hal.inria.fr/hal-01245888

DOI: 10.1007/978-3-662-46669-8_17

Affiliations:

Links toward previous steps (curation, corpus...)

to stream Hal, to step Corpus: 000503
to stream Hal, to step Curation: 000503
to stream Hal, to step Checkpoint: 000165
to stream Main, to step Merge: 000204
to stream Main, to step Curation: 000204
to stream Main, to step Exploration: 000204
to stream France, to step Extraction: 000145

Links to Exploration step

Hal:hal-01245888

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Refinement Types for Incremental Computational Complexity</title>
<author><name sortKey="Cicek, Ezgi" sort="Cicek, Ezgi" uniqKey="Cicek E" first="Ezgi" last="Çiçek">Ezgi Çiçek</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-105111" status="VALID">          <orgName>Max Planck Institute for Software Systems</orgName>
          <orgName type="acronym">MPI Software systems</orgName>
          <desc>            <address>              <addrLine>Max Planck Institute for Software Systems Wartburg Martin-Luther-Straße 12 D-66111 Saarbrücken Germany</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.mpi-sws.org/index_noflash.php?n=contact</ref>
          </desc>
          <listRelation>            <relation active="#struct-300044" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID">          <orgName>Max-Planck-Institut</orgName>
          <desc>            <address>              <country key="DE"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Garg, Deepak" sort="Garg, Deepak" uniqKey="Garg D" first="Deepak" last="Garg">Deepak Garg</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-105111" status="VALID">          <orgName>Max Planck Institute for Software Systems</orgName>
          <orgName type="acronym">MPI Software systems</orgName>
          <desc>            <address>              <addrLine>Max Planck Institute for Software Systems Wartburg Martin-Luther-Straße 12 D-66111 Saarbrücken Germany</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.mpi-sws.org/index_noflash.php?n=contact</ref>
          </desc>
          <listRelation>            <relation active="#struct-300044" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID">          <orgName>Max-Planck-Institut</orgName>
          <desc>            <address>              <country key="DE"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Acar, Umut" sort="Acar, Umut" uniqKey="Acar U" first="Umut" last="Acar">Umut Acar</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-67135" status="VALID">          <orgName>Carnegie Mellon University [Pittsburgh]</orgName>
          <orgName type="acronym">CMU</orgName>
          <desc>            <address>              <addrLine>5000 Forbes Ave,  Pittsburgh, PA 15213</addrLine>
              <country key="US"></country>
            </address>
            <ref type="url">http://www.cmu.edu/</ref>
          </desc>
        </hal:affiliation>
<country>États-Unis</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01245888</idno>
<idno type="halId">hal-01245888</idno>
<idno type="halUri">https://hal.inria.fr/hal-01245888</idno>
<idno type="url">https://hal.inria.fr/hal-01245888</idno>
<idno type="doi">10.1007/978-3-662-46669-8_17</idno>
<date when="2015-04-11">2015-04-11</date>
<idno type="wicri:Area/Hal/Corpus">000503</idno>
<idno type="wicri:Area/Hal/Curation">000503</idno>
<idno type="wicri:Area/Hal/Checkpoint">000165</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000165</idno>
<idno type="wicri:Area/Main/Merge">000204</idno>
<idno type="wicri:Area/Main/Curation">000204</idno>
<idno type="wicri:Area/Main/Exploration">000204</idno>
<idno type="wicri:Area/France/Extraction">000145</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Refinement Types for Incremental Computational Complexity</title>
<author><name sortKey="Cicek, Ezgi" sort="Cicek, Ezgi" uniqKey="Cicek E" first="Ezgi" last="Çiçek">Ezgi Çiçek</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-105111" status="VALID">          <orgName>Max Planck Institute for Software Systems</orgName>
          <orgName type="acronym">MPI Software systems</orgName>
          <desc>            <address>              <addrLine>Max Planck Institute for Software Systems Wartburg Martin-Luther-Straße 12 D-66111 Saarbrücken Germany</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.mpi-sws.org/index_noflash.php?n=contact</ref>
          </desc>
          <listRelation>            <relation active="#struct-300044" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID">          <orgName>Max-Planck-Institut</orgName>
          <desc>            <address>              <country key="DE"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Garg, Deepak" sort="Garg, Deepak" uniqKey="Garg D" first="Deepak" last="Garg">Deepak Garg</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-105111" status="VALID">          <orgName>Max Planck Institute for Software Systems</orgName>
          <orgName type="acronym">MPI Software systems</orgName>
          <desc>            <address>              <addrLine>Max Planck Institute for Software Systems Wartburg Martin-Luther-Straße 12 D-66111 Saarbrücken Germany</addrLine>
              <country key="FR"></country>
            </address>
            <ref type="url">http://www.mpi-sws.org/index_noflash.php?n=contact</ref>
          </desc>
          <listRelation>            <relation active="#struct-300044" type="direct"></relation>
          </listRelation>
        <tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID">          <orgName>Max-Planck-Institut</orgName>
          <desc>            <address>              <country key="DE"></country>
            </address>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Acar, Umut" sort="Acar, Umut" uniqKey="Acar U" first="Umut" last="Acar">Umut Acar</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-67135" status="VALID">          <orgName>Carnegie Mellon University [Pittsburgh]</orgName>
          <orgName type="acronym">CMU</orgName>
          <desc>            <address>              <addrLine>5000 Forbes Ave,  Pittsburgh, PA 15213</addrLine>
              <country key="US"></country>
            </address>
            <ref type="url">http://www.cmu.edu/</ref>
          </desc>
        </hal:affiliation>
<country>États-Unis</country>
</affiliation>
</author>
</analytic>
<idno type="DOI">10.1007/978-3-662-46669-8_17</idno>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">With recent advances, programs can be compiled to efficiently respond to incremental input changes. However, there is no language level support for reasoning about the time complexity of incremental updates. Motivated by this gap, we present CostIt, a higher-order functional language with a lightweight refinement type system for proving asymptotic bounds on incremental computation time. Type refinements specify which parts of inputs and outputs may change, as well as dynamic stability, a measure of time required to propagate changes to a program's execution trace, given modified inputs. We prove our type system sound using a new step-indexed cost semantics for change propagation and demonstrate the precision and generality of our technique through examples.</div>
</front>
</TEI>
<affiliations><list><country><li>Allemagne</li>
<li>France</li>
<li>États-Unis</li>
</country>
<orgName><li>Société Max-Planck</li>
</orgName>
</list>
<tree><country name="France"><noRegion><name sortKey="Cicek, Ezgi" sort="Cicek, Ezgi" uniqKey="Cicek E" first="Ezgi" last="Çiçek">Ezgi Çiçek</name>
</noRegion>
<name sortKey="Garg, Deepak" sort="Garg, Deepak" uniqKey="Garg D" first="Deepak" last="Garg">Deepak Garg</name>
</country>
<country name="États-Unis"><noRegion><name sortKey="Acar, Umut" sort="Acar, Umut" uniqKey="Acar U" first="Umut" last="Acar">Umut Acar</name>
</noRegion>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Amérique/explor/PittsburghV1/Data/France/Analysis

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000145 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/France/Analysis/biblio.hfd -nk 000145 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Amérique
   |area=    PittsburghV1
   |flux=    France
   |étape=   Analysis
   |type=    RBID
   |clé=     Hal:hal-01245888
   |texte=   Refinement Types for Incremental Computational Complexity
}}

This area was generated with Dilib version V0.6.38.
Data generation: Fri Jun 18 17:37:45 2021. Site generation: Fri Jun 18 18:15:47 2021

	Serveur d'exploration sur Pittsburgh
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur Pittsburgh

Refinement Types for Incremental Computational Complexity

Refinement Types for Incremental Computational Complexity

Source :

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri