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

• Type: Journal
• Year: 2011
• Where: CORR
• Authors: Ugo Dal Lago, Marco Gaboardi
• Keywords: CORR 2011, Dependent Types, Education, Linear Dependent Types, PCF Programs