Linear Dependent Types and Relative Completeness

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.

44 pages, 1 figure

Cited by in corpus (13)

• Intersection Types and (Positive) Almost-Sure Termination
• Syntax and Semantics of Linear Dependent Types
• From bounded affine types to automatic timing analysis
• Higher-Order Bayesian Networks, Exactly (Extended version)
• Denotational semantics as a foundation for cost recurrence extraction for functional languages
• The Geometry of Types (Long Version)
• Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order (Long Version)
• Probabilistic Termination by Monadic Affine Sized Typing (Long Version)
• Linear Dependent Types in a Call-by-Value Scenario (Long Version)
• Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics
• Raising Expectations: Automating Expected Cost Analysis with Types
• Automated Sized-Type Inference and Complexity Analysis
• A Categorical Semantics for Linear Logical Frameworks