A Simplified Account of the Metatheory of Linear LF

We present a variant of the linear logical framework LLF that avoids the restriction l-typed terms 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 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.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Joseph Vanderwaart, Karl Crary
• Keywords: Definitional Equality, Definitional Equality Judgments, ENTCS 2002, Linear Logical Framework