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. Additionally, the host language's
evaluation for expressions is defined by matching values rather
than expecting exact forms, with matching happening through
projection. For example, a list cons that projects
to a record can be used for record field accesses.
The reason it defines evaluation through matching is to support its projection constraints for evaluation, which require an expression's projection to evaluate whenever it does, and to a related value. This is a middle ground in strictness of projection constraints between the examples with loose constraints on evaluation and strict constraints on evaluation, which both implement roughly the same underlying language with differing projection constraints. Having three versions of very similar languages 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 constructs with natural definitions of their semantics, but not as many as either of the other versions, due to stricter projection constraints than the former and the lack of a way to nest statements inside expressions on the other. However, as a tradeoff for fewer constructs extensions can introduce, we find we can prove more about evaluation in extensions than the version with loose constraints, as we see in the translation extension, where we can prove the translation evaluates if the original does.