TY - JOUR
T1 - Linear dependent types and relative completeness
AU - Lago, Ugo Dal
AU - Gaboardi, Marco
PY - 2012/10/23
Y1 - 2012/10/23
N2 - A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behavior 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. dlPCF 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.
AB - A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behavior 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. dlPCF 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.
UR - http://www.scopus.com/inward/record.url?scp=84868095512&partnerID=8YFLogxK
M3 - Article
AN - SCOPUS:84868095512
VL - 8
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
IS - 4
M1 - 11
ER -