A two-level syntax specifies the binding-time properties of each syntactic construct [27]. Two-level terms (see Fig. 5) have the dynamic constructs underlined. The specializer statically reduces every construct which is not underlined.
Some constructs come in more than two variants, i.e., function application, abstraction, eval, and apply. For function application and abstraction we must distinguish two different forms of static functions: The standard (lambda ...) constructs a plain static function which cannot be memoized. The alternative ( ...) constructs a memoizable function which the specializer represents differently (see Sec. 3.5). The companion (@ ...) and ( ...) perform application of plain functions and memoizable functions, respectively. The same holds for variadic abstractions and ( ...).
In addition to the underlined and non-underlined versions of eval and apply (with the standard meaning), there exist doubly underlined versions where eval lifts a static piece of code into a dynamic context and apply applies a dynamic function to a (static) list of dynamic elements as explained in Sec. 3.1 and 3.2.
Together with the two-level terms we introduce a type system which captures a congruence criterion [21]. In a well-typed two-level term, each static construct only refers to static data. Therefore, all static constructs can be statically reduced and all remaining constructs are dynamic.