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.
- Implicit computational complexity
- Realizability model