Computer Science Department
School of Computer Science, Carnegie Mellon University
A Simplified Account of the Metatheory of Linear LF
Joseph C. Vanderwaart, Karl Crary
Keywords: Logical frameworks, type theory, linear logic
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 lambda-abstraction at the level of families.
We abandon the use of beta-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 definitional 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.