For semantic verification, some translation relations require more static information about variables in their typing/kind context. For example:
Inlining: which variables were let-bound and what was their RHS
Dead code, let-reordering: what was the strictness of binders? (to determine purity)
This information is statically available. We could either enrich the typing derivations with this information, which is conceptually simple, but will make the typing rules much noisier. Instead, defining separate environments and relations that make them "line up" (variable names) seems more modular.
Corresponding verification then needs to consider open terms with "suitable" substitutions, which can depend not only on the typing context, but also on this additional static information (e.g. non-strict binders can have arbitrary terms in the substitution whereas strict binders will have values).
For semantic verification, some translation relations require more static information about variables in their typing/kind context. For example:
This information is statically available. We could either enrich the typing derivations with this information, which is conceptually simple, but will make the typing rules much noisier. Instead, defining separate environments and relations that make them "line up" (variable names) seems more modular.
Corresponding verification then needs to consider open terms with "suitable" substitutions, which can depend not only on the typing context, but also on this additional static information (e.g. non-strict binders can have arbitrary terms in the substitution whereas strict binders will have values).