Redundancy Elimination for LF

  • Reed J
  • 5


    Mendeley users who have this article in their library.
  • 2


    Citations of this article.


We present a type system extending the dependent type theory LF, whose terms are more amenable to compact representation. This is achieved by carefully omitting certain subterms which are redundant in the sense that they can be recovered from the types of other subterms. This system is capable of omitting more redundant information than previous work in the same vein, because of its uniform treatment of higher-order and first-order terms. Moreover the 'recipe' for reconstruction of omitted information is encoded directly into annotations on the types in a signature. This brings to light connections between bidirectional (synthesis vs. checking) typing algorithms of the object language on the one hand, and the bidirectional flow of information in the ambient encoding language. The resulting system is a compromise seeking to retain both the effectiveness of full unification-based term reconstruction such as is found in implementation practice, and the logical simplicity of pure LF. © 2008 Elsevier B.V. All rights reserved.

Author-supplied keywords

  • Bidirectional Type Checking
  • Dependent Type Theory
  • Proof Compression

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Jason Reed

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free