The Twelf Proof Assistant

    Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

    Abstract

    Logical framework research is based on the philosophical point of view that it should be possible to capture mathematical concepts such as proofs, logics, and meaning in a formal system — directly, adequately (in the sense that there are no spurious or exotic witnesses), and without having to commit to a particular logical theory. Instead of working with one general purpose representation language, we design special purpose logical frameworks for capturing reoccurring concepts for special domains, such as, for example, variable renaming, substitution application, and resource management for programming language theory. Most logical frameworks are based on constructive type theories, such as Isabelle (on the simply-typed λ-calculus), LF [HHP93] (on the dependently typed λ-calculus), and LLF (on a linearly typed λ-calculus). The representational strength of the logical framework stems from the choice of definitional equality on terms. For example, α-conversion models the tacit renaming of variables, β-contraction models substitution application, and η-expansion guarantees the adequacy of encodings.
    Original languageEnglish
    Title of host publicationProceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics
    Number of pages83
    PublisherSpringer Publishing Company
    Publication date2009
    Pages79
    ISBN (Print)978-3-642-03358-2
    Publication statusPublished - 2009
    EventTheorem Proving in Higher Order Logics - Munich, Germany
    Duration: 17 Aug 200920 Aug 2009
    Conference number: 22

    Conference

    ConferenceTheorem Proving in Higher Order Logics
    Number22
    Country/TerritoryGermany
    CityMunich
    Period17/08/200920/08/2009
    SeriesLecture Notes In Computer Science
    Volume5674
    ISSN2078-0958

    Keywords

    • Logical frameworks
    • Constructive type theories
    • Definitional equality
    • Programming language theory
    • Formal systems

    Cite this