CMU-CS-01-154
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-01-154
A Simplified Account of the Metatheory of Linear LF
Joseph C. Vanderwaart, Karl Crary
April 2002
CMU-CS-01-154.ps
CMU-CS-01-154.pdf
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.
44 pages
|