Multi-Level Lambda-Calculi: An Algebraic Description

Abstract. 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 two-level structure and the corresponding inference rules. We therefore formulate a number of existing systems in a common framework. This is done in such a way as to conceal those differences between the systems that are not essential for the multi-level ideas (like whether or not one restricts the domain of the type environment to the free identifiers of the expression) and thereby to reveal the deeper similarities and differences. In their most general guise the multi-level -calculi allow multi-level structures that are not restricted to (possibly finite) linear orders and thereby generalise previous treatments in the literature.

• Type: Conference
• Year: 1996
• Where: DAGSTUHL
• Authors: Flemming Nielson, Hanne Riis Nielson
• Keywords: Allow Multi-level Structures, Corresponding Inference Rules, DAGSTUHL 1996, DAGSTUHL 2007, Two-level -calculi