Multi-Level Languages: a Descriptive Framework

Abstract

Two-level lambda-calculi have been utilised for applications such as partial evalu- ation, abstract interpretation and code generation. Each of these applications pose different demands on the exact details of the two-level structure and the corresponding inference rules. We therefore formulate a number of existing systems in a common framework so as to conceal those differences between the systems that are not essential for the multi-level ideas, and so as to reveal the deeper similarities and differences. The multi-level lambda-calculi defined here allow multi-level structures that are not restricted to the (possibly finit) linear orders found in most of the literature. Finally, we generalise our approach so as to be applicable to a much wider class of programming languages.