Linear Dependent Types and Relative Completeness

TL;DR

This paper introduces dlPCF, a linear dependent type system for the lambda calculus with recursion, capable of capturing both functional and some intensional properties like evaluation complexity, with a focus on soundness and relative completeness.

Contribution

It presents dlPCF, a novel type system combining linear logic and dependent types, and proves its soundness and relative completeness for higher-order recursion.

Findings

dlPCF precisely captures functional behavior of PCF programs

dlPCF can also analyze evaluation complexity using Krivine's Machine

The system's completeness can be tuned via index terms for tractability

Abstract

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.