Two-level languages for program optimization

Two-level languages incorporate binding time information inside types, that is, whether a piece of code is completely known at compile-time, or needs some more inputs and can be evaluated only at run-time. We consider the use of 2-level languages in the framework of partial evaluation, and use a 2-level version of the simply typed lambda calculus with recursion. We give an operational semantics, an equational theory and a denotational semantics, that give an account of the distinction between compilation and execution phases. An adequacy theorem is given to relate the two semantics, showing in particular how they agree on non-termination at compile time. We finally give a more refined model using functor categories. (C) 2003 Elsevier B.V. All rights reserved.