Linear dependent types and relative completeness

Ugo Dal Lago, Marco Gaboardi

    Research output: Contribution to journalArticle

    7 Citations (Scopus)

    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 behavior 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.
    Original languageEnglish
    Article number11
    JournalLogical Methods in Computer Science
    Volume8
    Issue number4
    Publication statusPublished - 23 Oct 2012

    Fingerprint

    Completeness
    Acoustic waves
    Linear Logic
    Dependent
    Lambda Calculus
    Tractability
    Recursion
    Higher Order
    Output
    Term
    Sound
    Language

    Cite this

    Lago, Ugo Dal ; Gaboardi, Marco. / Linear dependent types and relative completeness. In: Logical Methods in Computer Science. 2012 ; Vol. 8, No. 4.
    @article{ba2f2427146f4829947034c1ec97249e,
    title = "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 behavior 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.",
    author = "Lago, {Ugo Dal} and Marco Gaboardi",
    year = "2012",
    month = "10",
    day = "23",
    language = "English",
    volume = "8",
    journal = "Logical Methods in Computer Science",
    issn = "1860-5974",
    publisher = "IfCoLog",
    number = "4",

    }

    Linear dependent types and relative completeness. / Lago, Ugo Dal; Gaboardi, Marco.

    In: Logical Methods in Computer Science, Vol. 8, No. 4, 11, 23.10.2012.

    Research output: Contribution to journalArticle

    TY - JOUR

    T1 - Linear dependent types and relative completeness

    AU - Lago, Ugo Dal

    AU - Gaboardi, Marco

    PY - 2012/10/23

    Y1 - 2012/10/23

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

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

    UR - http://www.scopus.com/inward/record.url?scp=84868095512&partnerID=8YFLogxK

    M3 - Article

    VL - 8

    JO - Logical Methods in Computer Science

    JF - Logical Methods in Computer Science

    SN - 1860-5974

    IS - 4

    M1 - 11

    ER -