Prescriptive Frameworks for Multi-Level Lambda-Calculi
Flemming Nielson, Hanne Riis Nielson · 1997
Two-level -calculi have been heavily utilised for applications such as partial evaluation, abstract interpretation and code generation. Each of these applications pose different demands on the exact details of the twolevel structure and the corresponding inference rules. In a previous paper we have developed a descriptive framework for characterising the key ingredients used in the various applications. Based on the insights offered by this characterisation we now develop a prescriptive framework that offers firm guidelines on what we regard as "good" definitions of multi-level lambda-calculi. 1 Introduction The literature has seen quite a number of multi-level languages used for different purposes: partial evaluation [5], code generation [8] and abstract interpretation [7]. At the surface, they all seem very different and in a recent paper [11] we performed a careful descriptive study of the multi-level lambda-calculi found in the literature. This allowed us to highlight a number ...