Explicit context

From The Twelf Project
Jump to: navigation, search

Explicit contexts are an alternative technique for encoding an object language. Standard practice is to use higher-order judgments in order to implicitly use the LF context as the context for the object language semantics. While this affords many benefits, there are a number of proof techniques (such as hereditary substitution for dependently typed languages) which require isolating an entry in the middle of the object language context. This is not possible in general using higher-order judgments for languages whose context does not admit exchange.

It is possible to prove such theorems in an encoding of the object language semantics with an explicit reconstruction of the context. In order to maximally enjoy the benefits of higher-order judgments, standard practice is to use the explicit context system only as necessary, and prove theorems that convert derivations from the implicit and explicit systems.

This technique was used in the code associated with Towards a Mechanized Metatheory of Standard ML.

Although explicit contexts are the most general technique for proving theorems that mention entries in the middle of contexts that do not admit exchange, very often there are tricks to avoid using explicit contexts. A section of the page on substitution lemmas illustrates one such technique.


This page is incomplete. We should expand it.