This host language defines a large imperative language defining programs as lists of functions, with one function being designated as the main function. It defines typing and evaluation, with the latter defined as executing the main function, producing a list of values as printed output.
The host language here introduces very strict projection constraints for evaluation, requiring extensions to define the semantics of their new constructs exactly the same as their projections, with expressions needing to evaluate to exactly the same values as their projections do and extension constructs evaluating if and only if their projections do. Together with the examples of loose constraints on evaluation and evaluation through matching, which both implement roughly the same underlying language with differing projection constraints, it allows us to explore how differences in projection constraints and constructs included in the host language affect what we can introduce and prove for extensions.
In this version of the language, we find we can introduce a lot of constructs despite the strictness of the projection constraints because the host language includes a construct for nesting statements in expressions, but their semantic definitions can be more awkward than in the other languages. In exchange for this semantic awkwardness, however, we can prove a lot about evaluation in extensions. In particular, in the translation extension, we find we can prove the translation evaluates if and only if the original program evaluates, and with the same evaluation results.