Skip to Main content Skip to Navigation
New interface
Journal articles

Linear Dependent Types in a Call-by-Value Scenario

Ugo Dal Lago 1, 2 Barbara Petit 3 
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Linear dependent types allow 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 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 behavior of terms can be derived, provided all true index term inequalities can be used as assumptions.
Document type :
Journal articles
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download
Contributor : Davide Sangiogi Connect in order to contact the contributor
Submitted on : Tuesday, November 26, 2013 - 10:46:37 AM
Last modification on : Tuesday, October 25, 2022 - 4:23:31 PM
Long-term archiving on: : Monday, March 3, 2014 - 4:11:45 PM


Files produced by the author(s)




Ugo Dal Lago, Barbara Petit. Linear Dependent Types in a Call-by-Value Scenario. Science of Computer Programming, 2013, ⟨10.1016/j.scico.2013.07.010⟩. ⟨hal-00909317⟩



Record views


Files downloads