Linear dependent types in a call-by-value scenario

• A type system for complexity analysis of higher-order functional programs.
• Extend previous, related, work to an applied, call-by-value, lambda-calculus.
• The type system is not only sound, but relatively complete.
• We provide fully-developed nontrivial examples of complexity analyses.

Linear dependent types were introduced recently (Dal Lago and Gaboardi, 2012) [26] as a formal system that allows to precisely capture both the extensional behavior and the time complexity of λ-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 computation. A system of linear dependent types for Plotkin’s  is introduced, called , whose types reflect the complexity of evaluating terms in the  machine.  is proved to be sound, but also relatively complete: every true statement about the extensional and intentional behavior of terms can be derived, provided all true index term inequalities can be used as assumptions.