Realizability models for a linear dependent PCF

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 - https://www.scopus.com/pages/publications/84945288732

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 -