Realizability models for a linear dependent PCF

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.