Explicit Contexts in LF (Revised)

The standard methodology for representing deductive systems in LF identifies the object's language's context with the LF context. Consequently, any variable dealt with explicitly by any judgement or metatheorem must be last in the context. When the object language is dependently typed, this can pose a problem for establishing some metatheoretic results, since dependent hypotheses cannot be re-ordered at will. This paper presents a general technique that addresses such problems, based on representing the object language's context as an explicit object in LF while retaining the use of higher-order representation for the object language's syntax. A central result is that it is possible to convert between explicit and implicit contexts, which makes it feasible to use the standard methodology for most developments, but use explicit contexts where necessary. We do not propose any extensions to LF; the technique can be utilized in standard LF.