Realizability models for a linear dependent PCF

Aloïs Brunel; Marco Gaboardi

doi:10.1016/j.tcs.2015.03.005

Realizability models for a linear dependent PCF

Aloïs Brunel, Marco Gaboardi (Lead / Corresponding author)

Computing

Research output: Contribution to journal › Article › peer-review

Abstract

Recently, Dal Lago and Gaboardi have proposed a type system, named dℓ. PCF as a framework for implicit computational complexity. dℓ. PCF is a non-standard type system for PCF programs which is relatively complete with respect to quantitative properties thanks to the use of linear types inspired by Bounded linear logic and dependent types à la Dependent ML. In this work, we adapt the framework of quantitative realizability and obtain a model for dℓ. PCF. The quantitative realizability model aims at a better understanding of dℓ. PCF type decorations and at giving an abstract semantic proof of intensional soundness.

Original language	English
Pages (from-to)	55-70
Number of pages	16
Journal	Theoretical Computer Science
Volume	585
Early online date	9 Mar 2015
DOIs	https://doi.org/10.1016/j.tcs.2015.03.005
Publication status	Published - 20 Jun 2015

Keywords

Implicit computational complexity
Realizability model

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1016/j.tcs.2015.03.005Licence: Elsevier User Licence

Cite this

@article{057ae60f91ae4456944a8567cf5129c9,

title = "Realizability models for a linear dependent PCF",

abstract = "Recently, Dal Lago and Gaboardi have proposed a type system, named dℓ. PCF as a framework for implicit computational complexity. dℓ. PCF is a non-standard type system for PCF programs which is relatively complete with respect to quantitative properties thanks to the use of linear types inspired by Bounded linear logic and dependent types {\`a} la Dependent ML. In this work, we adapt the framework of quantitative realizability and obtain a model for dℓ. PCF. The quantitative realizability model aims at a better understanding of dℓ. PCF type decorations and at giving an abstract semantic proof of intensional soundness.",

keywords = "Implicit computational complexity, Realizability model",

author = "Alo{\"i}s Brunel and Marco Gaboardi",

year = "2015",

month = jun,

day = "20",

doi = "10.1016/j.tcs.2015.03.005",

language = "English",

volume = "585",

pages = "55--70",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

}

TY - JOUR

T1 - Realizability models for a linear dependent PCF

AU - Brunel, Aloïs

AU - Gaboardi, Marco

PY - 2015/6/20

Y1 - 2015/6/20

N2 - Recently, Dal Lago and Gaboardi have proposed a type system, named dℓ. PCF as a framework for implicit computational complexity. dℓ. PCF is a non-standard type system for PCF programs which is relatively complete with respect to quantitative properties thanks to the use of linear types inspired by Bounded linear logic and dependent types à la Dependent ML. In this work, we adapt the framework of quantitative realizability and obtain a model for dℓ. PCF. The quantitative realizability model aims at a better understanding of dℓ. PCF type decorations and at giving an abstract semantic proof of intensional soundness.

AB - Recently, Dal Lago and Gaboardi have proposed a type system, named dℓ. PCF as a framework for implicit computational complexity. dℓ. PCF is a non-standard type system for PCF programs which is relatively complete with respect to quantitative properties thanks to the use of linear types inspired by Bounded linear logic and dependent types à la Dependent ML. In this work, we adapt the framework of quantitative realizability and obtain a model for dℓ. PCF. The quantitative realizability model aims at a better understanding of dℓ. PCF type decorations and at giving an abstract semantic proof of intensional soundness.

KW - Implicit computational complexity

KW - Realizability model

UR - http://www.scopus.com/inward/record.url?scp=84945288732&partnerID=8YFLogxK

U2 - 10.1016/j.tcs.2015.03.005

DO - 10.1016/j.tcs.2015.03.005

M3 - Article

AN - SCOPUS:84945288732

SN - 0304-3975

VL - 585

SP - 55

EP - 70

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -

Realizability models for a linear dependent PCF

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this