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.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2013, 〈10.1016/j.scico.2013.07.010〉
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00909317
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 10:46:37
Dernière modification le : mardi 16 janvier 2018 - 16:10:38
Document(s) archivé(s) le : lundi 3 mars 2014 - 16:11:45

Fichier

scp2013.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

235

Téléchargements de fichiers

147