Hostname: page-component-599cfd5f84-56l7z Total loading time: 0 Render date: 2025-01-07T07:49:36.214Z Has data issue: false hasContentIssue false
  • English
  • Français

From operational semantics to abstract machines

Published online by Cambridge University Press:  04 March 2009

John Hannan  and
Dale Miller
John Hannan
Affiliation:
Department of Computer Science, The Pennsylvania State University, University Park, PA 16802, USA. ([email protected])
Dale Miller
Affiliation:
Computer and Information Science, University of Pennsylvania, Philadelphia, PA 19104–6389, USA. ([email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

We consider the problem of mechanically constructing abstract machines from operational semantics, producing intermediate-level specifications of evaluators guaranteed to be correct with respect to the operational semantics. We construct these machines by repeatedly applying correctness-preserving transformations to operational semantics until the resulting specifications have the form of abstract machines. Though not automatable in general, this approach to constructing machine implementations can be mechanized, providing machine-verified correctness proofs. As examples, we present the transformation of specifications for both call-by-name and call-by-value evaluation of the untyped λ-calculus into abstract machines that implement such evaluation strategies. We also present extensions to the call-by-value machine for a language containing constructs for recursion, conditionals, concrete data types, and built-in functions. In all cases, the correctness of the derived abstract machines follows from the (generally transparent) correctness of the initial operational semantic specification and the correctness of the transformations applied.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 2 , Issue 4 , December 1992 , pp. 415 - 459
Copyright
Copyright © Cambridge University Press 1992

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

de Bruijn, N. (1972) Lambda calculas notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indag. Math., 34(5) 381–392.CrossRefGoogle Scholar
Cardelli, L. (1984) Compiling a functional language. In: 1984 Symposium on LISP and Functional Programming, ACM, 208–217.Google Scholar
Cousineau, G., Curien, P.-L., and Mauny, M. (1987) The categorical abstract machine. The Science of Programming, 8(2) 173–202.CrossRefGoogle Scholar
Church, A. (1940) A formulation of the simple theory of types. Journal of Symbolic Logic, 5 56–68.CrossRefGoogle Scholar
Curien, P.-L. (1969) The λρ-calculus: An Abstract Framework for Environment Machines. Technical Report, LIENS–CNRS.Google Scholar
Gentzen, G. (1969) Investigations into logical deduction. In: Szabo, M., editor, The collected Papers of Gerhard Gentzen, North-Holland Publishing Co, 68–131.Google Scholar
Girard, J-Y. (1986) The system F of variable types: fifteen years later. Theoretical Computer Science, 45 159–192.CrossRefGoogle Scholar
Hannan, J. (1990) Investigating a Proof-Theoretic Meta-Language for Functional Programs. PhD thesis, University of Pennsylvania.Google Scholar
Hannan, J. (1991) Staging transformations for abstract machines. In Hudak, P. and Jones, N., editors, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation, ACM Press, 130–141.Google Scholar
Harper, R., Honsell, F., and Poltkin, G. (1987) A framework for defining logics. In: Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 194–204.Google Scholar
Huet, G. and Oppen, D. (1980) Equations and rewrite rules: a survay. In: Book, R., editor, Formal Language Theory: Perspectives and Open Problems, Academic Press, 349–405.Google Scholar
Howe, D. (1991) On computational open-endedness in Martin-Löf's type theory. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 162–172.Google Scholar
Hannan, J. and Pfenning, F. (1992) Compiler verification in LF. In: Scedrov, Andre, editor, Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 407–418.Google Scholar
Hindley, J. R. and Seldin, J. P. (1986) Introduction to Combinators and λ-calculus. Cambridge University Press.Google Scholar
Kahn, G. (1987) Natural semantics. In: Proceedings of the Symposium on Theoretical Aspects of Computer Science. Springer-Verlag LNCS, 247 22–39.Google Scholar
Landin, P. J. (1964) The mechanical evaluation of expressions. Computer Journal, 6(5) 308–320.Google Scholar
Martin-Löf, P. (1984) Intuitionistic Type Theory. Studies in Proof Theory Lecture Notes, BIBLIOPOLIS, Napoli.Google Scholar
Martin-Löf, P. (1985) Constructive Mathematics and Computer Programming, Prentice-Hall, 167–184.Google Scholar
Milner, R., Tofte, M. and Harper, R. (1990) The Definition of Standard ML. MIT Press.Google Scholar
Nadathur, G. and Milner, D. (1988) An overview of λProlog. In: Bowen, K. and Kowalski, R., editors, Fifth International Conference and Symposium on Logic Programming, MIT Press, 810–827.Google Scholar
Nielson, F. and Nielson, H. (1988) Two-level semantics and code generation. Theoretical Computer Science, 56 59–133.CrossRefGoogle Scholar
Pfenning, F. (1991) Logic programming in the LF logical framework. In: Huet, Génard and Plotkin, Gordon D., editors, Logical Frameworks, Cambridge University Press, 66–78.Google Scholar
Plotkin, G. (1976) Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(1) 125–159.CrossRefGoogle Scholar
Plotkin, G. (1981) A Structural Approach to Operational Semantics. DAIMI FN-19, Aarhus Univversity, Aarhus, Denmark.Google Scholar
Prawitz, D. (1965) Natural Deduction. Almqvist & Wiksell, Uppsala.Google Scholar
da Silva, F. (1990) Towards a Formal Framework for Evaluation of Operational Semantics Specifications. LFCS Report ECS–LFCS–90–126, Edinburgh University.Google Scholar
Wand, M. (1982) Deriving target code as a representation of continuation semantics. ACM Trans.on Programming Languages and Systems, 4(3) 496–517.Google Scholar