CMUCS01154
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS01154
A Simplified Account of the Metatheory of Linear LF
Joseph C. Vanderwaart, Karl Crary
April 2002
CMUCS01154.ps
CMUCS01154.pdf
Keywords: Logical frameworks, type theory, linear logic
We present a variant of the linear logical framework LLF that
avoids the restriction that welltyped forms be in precanonical
form and adds lambdaabstraction at the level of families.
We abandon the use of betaconversion as definitional equality
in favor of a set of typed definitional equality judgments
that include rules for parallel conversion and extensionality.
We show typechecking is decidable by giving an algorithm to
decide definitional equality for welltyped 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 welltyped terms and may therefore ignore the distinction
between intuitionistic and linear hypotheses.
44 pages
