Realizability models for a linear dependent PCF

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

Research output: Contribution to journalArticlepeer-review


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 languageEnglish
Pages (from-to)55-70
Number of pages16
JournalTheoretical Computer Science
Early online date9 Mar 2015
Publication statusPublished - 20 Jun 2015


  • Implicit computational complexity
  • Realizability model

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Realizability models for a linear dependent PCF'. Together they form a unique fingerprint.

Cite this