Carnegie Mellon University
Browse

A Simplified Account of the Metatheory of Linear LF

Download (272.78 kB)
journal contribution
posted on 2006-11-01, 00:00 authored by Joseph C. Vanderwaart, Karl Crary
We present a variant of the linear logical framework LLF that avoids the restriction that well-typed forms be in pre-canonical form and adds λ-abstraction at the level of families. We abandon the use of β-conversion as definitional equality in favor of a set of typed definitional equality judgments that include rules for parallel conversion and extensionality. We show type-checking is decidable by giving an algorithm to decide denfiitional equality for well-typed terms and showing the algorithm is sound and complete. The algorithm and the proof of its correctness are simplified by the fact that they apply only to well-typed terms and may therefore ignore the distinction between intuitionistic and linear hypotheses.

History

Publisher Statement

Appears in Theoretical Computer Science Volume 367, Issues 1-2, 24 November 2006, Pages 57-87

Date

2006-11-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC