Linear Dependent Types and Relative Completeness

Ugo Dal Lago 1, 2 Marco Gaboardi 1, 2, 3
Abstract : A system of linear dependent types for the lambda calculus with full higher-order recursion, called dℓPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dℓPCF is not only able to precisely capture the functional behaviour of PCF programs (i.e. how the output relates to the input) but also some of their intensional properties, namely the complexity of evaluating them with Krivine's Machine. dℓPCF is designed around dependent types and linear logic and is parametrized on the underlying language of index terms, which can be tuned so as to sacrifice completeness for tractability.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (4)
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00906347
Contributeur : Davide Sangiogi <>
Soumis le : mardi 19 novembre 2013 - 15:41:26
Dernière modification le : samedi 27 janvier 2018 - 01:30:40
Document(s) archivé(s) le : jeudi 20 février 2014 - 09:30:36

Fichier

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

Identifiants

  • HAL Id : hal-00906347, version 1

Collections

Citation

Ugo Dal Lago, Marco Gaboardi. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (4). 〈hal-00906347〉

Partager

Métriques

Consultations de la notice

420

Téléchargements de fichiers

258