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 loose projection constraints for evaluation, allowing extensions a lot of freedom in defining the semantics of their new constructs. Together with the examples of evaluation through matching and strict constraints on evaluation, 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 with natural definitions of their semantics. However, as a tradeoff for this freedom, we find we cannot prove much about evaluation in extensions, as we see in the translation extension.