Linear Dependent Types in a Call-by-Value Scenario (Long Version)

TL;DR

This paper extends linear dependent types to call-by-value evaluation, providing a type system for PCF that captures both behavior and complexity, and proves its soundness and relative completeness.

Contribution

It introduces dlPCFV, a linear dependent type system for call-by-value PCF, adapting the paradigm to the CEK machine evaluation model.

Findings

dlPCFV accurately captures evaluation complexity.

The system is sound and relatively complete.

It generalizes linear dependent types to call-by-value semantics.

Abstract

Linear dependent types allow to precisely capture both the extensional behaviour and the time complexity of lambda terms, when the latter are evaluated by Krivine's abstract machine. In this work, we show that the same paradigm can be applied to call-by-value evaluation. A system of linear dependent types for Plotkin's PCF is introduced, called dlPCFV, whose types reflect the complexity of evaluating terms in the so-called CEK machine. dlPCFV is proved to be sound, but also relatively complete: every true statement about the extensional and intentional behaviour of terms can be derived, provided all true index term inequalities can be used as assumptions.