Linear dependent types in a call-by-value scenario

Ugo Dal Lago 1, 2 Barbara Petit 2, 1
1 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 were introduced recently as a formal system that allows to precisely capture both the extensional behavior and the time com-plexity of λ-terms, when the latter are evaluated by Krivine's abstract ma-chine. 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 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.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2014, pp.24. 〈10.1145/2370776.2370792〉
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-01091610
Contributeur : Ugo Dal Lago <>
Soumis le : vendredi 5 décembre 2014 - 16:47:54
Dernière modification le : samedi 27 janvier 2018 - 01:31:49
Document(s) archivé(s) le : lundi 9 mars 2015 - 06:05:09

Fichier

main.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, 2014, pp.24. 〈10.1145/2370776.2370792〉. 〈hal-01091610〉

Partager

Métriques

Consultations de la notice

157

Téléchargements de fichiers

121