Skip to Main content Skip to Navigation
New interface
Journal articles

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 metadata

Cited literature [37 references]  Display  Hide  Download
Contributor : Davide Sangiogi Connect in order to contact the contributor
Submitted on : Tuesday, November 19, 2013 - 3:41:26 PM
Last modification on : Friday, November 18, 2022 - 9:23:44 AM
Long-term archiving on: : Thursday, February 20, 2014 - 9:30:36 AM


Files produced by the author(s)


  • HAL Id : hal-00906347, version 1



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



Record views


Files downloads