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 ORCID-iD; 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
    Accepted on: June 25, 2015
    Submitted on: December 29, 2011
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.3.2, F.3.1
    Fundings :
      Source : OpenAIRE Research Graph
    • PRACTICAL LIGHT TYPES FOR RESOURCE CONSUMPTION; Funder: European Commission; Code: 272487

    Linked data

    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.fscd.2021.31
    Source : ScholeXplorer IsCitedBy HANDLE 2066/236638
    • 10.4230/lipics.fscd.2021.31
    • 2066/236638
    • 2066/236638
    Tuple Interpretations for Higher-Order Complexity
    Kop, C. ; Vale, D. ; Kobayashi, N. ;

    11 Documents citing this article


    Consultation statistics

    This page has been seen 511 times.
    This article's PDF has been downloaded 261 times.