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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/hal-00906347
Contributor : Davide Sangiogi <>
Submitted on : Tuesday, November 19, 2013 - 3:41:26 PM
Last modification on : Thursday, July 4, 2019 - 3:56:24 PM
Long-term archiving on : Thursday, February 20, 2014 - 9:30:36 AM

File

1104.0193.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

467

Files downloads

446