Ugo Dal Lago ; Marco Gaboardi - Linear Dependent Types and Relative Completeness

lmcs:974 - Logical Methods in Computer Science, October 23, 2012, Volume 8, Issue 4 -
Linear Dependent Types and Relative Completeness

Authors: Ugo Dal Lago ; Marco Gaboardi

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 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. 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.

Volume: Volume 8, Issue 4
Published on: October 23, 2012
Submitted on: December 29, 2011
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.3.2, F.3.1


Consultation statistics

This page has been seen 389 times.
This article's PDF has been downloaded 177 times.