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 defined here allow multi-level structures that are not restricted to (possibly finite) linear orders and thereby generalise previous treatments in the literature.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
R. Glück and J. Jørgensen: Efficient Multi-level Generating Extensions for Program Specialization. PLILP'95, Springer Lecture Notes in Computer Science, vol. 982: pp. 259–278, 1995.
J. A. Goguen and J. W. Thatcher and E. G. Wagner: An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types. Current Trends in Programming Methodology, vol. 4, (R. T. Yeh, editor), Prentice-Hall, 1978.
F. Henglein and C. Mossin: Polymorphic Binding-Time Analysis. ESOP'94, Springer Lecture Notes in Computer Science, vol. 788: pp. 287–301, 1994.
N. D. Jones and P. Sestoft and H. Søndergaard: An Experiment in Partial Evaluation: the Generation of a Compiler Generator. Rewriting Techniques and Applications, Springer Lecture Notes in Computer Science, vol. 202: pp. 124–140, 1985.
N. D. Jones and F. Nielson: Abstract Interpretation: a Semantics-Based Tool for Program Analysis. Handbook of Logic in Computer Science, vol. 4: pp. 527–636, Oxford University Press, 1995.
J. C. Mitchell: Type Systems for Programming Languages. Handbook of Theoretical Computer Science: Formal Models and Semantics, vol. B: pp. 365–458, Elsevier Science Publishers (and MIT Press), 1990.
F. Nielson: Abstract Interpretation using Domain Theory. PhD thesis, University of Edinburgh, Scotland, 1984.
F. Nielson: Two-Level Semantics and Abstract Interpretation. Theoretical Computer Science — Fundamental Studies, vol. 69: pp. 117–242, 1989.
F. Nielson and H. R. Nielson: Two-level semantics and code generation. Theoretical Computer Science, vol. 56(1): pp. 59–133, 1988.
H. R. Nielson and F. Nielson: Automatic Binding Time Analysis for a Typed λcalculus. Science of Computer Programming, vol. 10: pp. 139–176, 1988.
F. Nielson and H. R. Nielson: Two-Level Functional Languages. Vol. 34 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1992.
F. Nielson and H. R. Nielson: Forced Transformations of Occam Programs. Information and Software Technology, vol. 34(2): pp. 91–96, 1992.
C. Strachey: The Varieties of Programming Languages. Technical Monograph PRG-10, Programming Research Group, University of Oxford, 1973.
M. Wirsing: Algebraic Specification. Handbook of Theoretical Computer Science: Formal Models and Semantics, vol. B: pp. 675–788, Elsevier (and MIT Press), 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nielson, F., Nielson, H.R. (1996). Multi-Level Lambda-Calculi: An algebraic description. In: Danvy, O., Glück, R., Thiemann, P. (eds) Partial Evaluation. Lecture Notes in Computer Science, vol 1110. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61580-6_17
Download citation
DOI: https://doi.org/10.1007/3-540-61580-6_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61580-4
Online ISBN: 978-3-540-70589-5
eBook Packages: Springer Book Archive