Sciweavers

Share
CORR
2011
Springer

Linear Dependent Types and Relative Completeness

8 years 14 days ago
Linear Dependent Types and Relative Completeness
—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
Ugo Dal Lago, Marco Gaboardi
Added 13 May 2011
Updated 13 May 2011
Type Journal
Year 2011
Where CORR
Authors Ugo Dal Lago, Marco Gaboardi
Comments (0)
books