Redundancy Elimination for LF

2Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.

Abstract

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.

Cite

CITATION STYLE

APA

Reed, J. (2008). Redundancy Elimination for LF. Electronic Notes in Theoretical Computer Science, 199, 89–106. https://doi.org/10.1016/j.entcs.2007.11.014

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free