Two-level,k-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 flamework. 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 A-calculi defined here allow multi-level structures that are not restricted to (possibly finite) linear orders and thereby generaiise previous treatments in the literature.
CITATION STYLE
Nielson, F., & Nielson, H. R. (1996). Multi-level lambda-calculi: An algebraic description. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1110, pp. 338–354). Springer Verlag. https://doi.org/10.1007/3-540-61580-6_17
Mendeley helps you to discover research relevant for your work.