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


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu