Multi-Level Lambda-Calculi: An algebraic description

  • Flemming Nielson
  • Hanne Riis Nielson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1110)


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.


Inference Rule Correct Treatment Partial Evaluation Abstract Interpretation Syntactic Category 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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.Google Scholar
  2. 2.
    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.Google Scholar
  3. 3.
    F. Henglein and C. Mossin: Polymorphic Binding-Time Analysis. ESOP'94, Springer Lecture Notes in Computer Science, vol. 788: pp. 287–301, 1994.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    F. Nielson: Abstract Interpretation using Domain Theory. PhD thesis, University of Edinburgh, Scotland, 1984.Google Scholar
  8. 8.
    F. Nielson: Two-Level Semantics and Abstract Interpretation. Theoretical Computer Science — Fundamental Studies, vol. 69: pp. 117–242, 1989.Google Scholar
  9. 9.
    F. Nielson and H. R. Nielson: Two-level semantics and code generation. Theoretical Computer Science, vol. 56(1): pp. 59–133, 1988.Google Scholar
  10. 10.
    H. R. Nielson and F. Nielson: Automatic Binding Time Analysis for a Typed λcalculus. Science of Computer Programming, vol. 10: pp. 139–176, 1988.Google Scholar
  11. 11.
    F. Nielson and H. R. Nielson: Two-Level Functional Languages. Vol. 34 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1992.Google Scholar
  12. 12.
    F. Nielson and H. R. Nielson: Forced Transformations of Occam Programs. Information and Software Technology, vol. 34(2): pp. 91–96, 1992.Google Scholar
  13. 13.
    C. Strachey: The Varieties of Programming Languages. Technical Monograph PRG-10, Programming Research Group, University of Oxford, 1973.Google Scholar
  14. 14.
    M. Wirsing: Algebraic Specification. Handbook of Theoretical Computer Science: Formal Models and Semantics, vol. B: pp. 675–788, Elsevier (and MIT Press), 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Flemming Nielson
    • 1
  • Hanne Riis Nielson
    • 1
  1. 1.DAIMIAarhus UniversityDenmark

Personalised recommendations