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 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.
Type de document :
Communication dans un congrès
Principles and Practice of Declarative Programming, (PPDP'12), 2012, Leuven, Belgium. ACM, pp.115--126, 2012, 〈10.1145/2370776.2370792〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00909371
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 11:08:14
Dernière modification le : vendredi 20 avril 2018 - 15:44:24

Lien texte intégral

Identifiants

Collections

Citation

Ugo Dal Lago, Barbara Petit. Linear dependent types in a call-by-value scenario. Principles and Practice of Declarative Programming, (PPDP'12), 2012, Leuven, Belgium. ACM, pp.115--126, 2012, 〈10.1145/2370776.2370792〉. 〈hal-00909371〉

Partager

Métriques

Consultations de la notice

314