Redundancy Elimination for LF

8 years 12 months ago
Redundancy Elimination for LF
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 unificationbased term reconstruction such as is found in implementation practice, and the logical simplicity of pure LF. ...
Jason Reed
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Authors Jason Reed
Comments (0)