Syntax

For our presentation we use higher-order recursion equations (see Fig. 1) in Scheme notation [22].

  

Figure 1: Syntax of the subject language

A definition can define a function of fixed arity or any value, for example a variadic function. An expression is either a variable V, a constant K, a conditional, an application of an external or built-in operator O, a procedure call, an abstraction of a function of fixed arity, a function application to a known number of arguments, an abstraction of a variadic function, a function application to an unknown number of arguments, eval, or call/cc. Among the operators we assume the constructors vcons and vnil, the selectors vcar and vcdr, and the constructor tests vnil? and vcons? to process argument lists. They correspond exactly to the usual list operators. Either a flow analysis could introduce them or we can interpret all standard list operators as argument list operators.