From Operational Semantics to Abstract Machines John Hannan Department of Computer Science University of Copenhagen Universitetsparken DK Copenhagen East Denmark dk Dale Miller Computer and Information Science University of Pennsylvania Philadelphia PA USA upenn edu

John Hannan

Description

Niveau: Supérieur, Doctorat, Bac+8
From Operational Semantics to Abstract Machines John Hannan Department of Computer Science, University of Copenhagen, Universitetsparken 1, DK-2100 Copenhagen East, Denmark. Dale Miller Computer and Information Science, University of Pennsylvania, Philadelphia, PA 19104-6389, USA. Received 16 October 1992 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. 1. Introduction The correctness of programming language implementations is an important issue con- fronting language designers and implementors.

• order quantification


• inference rules


• has proved


• logic permitting


• operational semantics


• specifications


• specifications provide


• abstract machine


• such semantic

Sujets

• Hannan
• Rule of inference
• Operational semantics
• Spécification
• Abstract machine

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 75
• Langue: English

Extrait

From Operational Semantics to Abstract

John Hannan Department of Computer Science, University of Copenhagen, Universitetsparken 1, DK-2100 Copenhagen East, Denmark. [e-mail]

Dale Miller Computer and Information Science, University of Pennsylvania, Philadelphia, PA 19104-6389, USA. [e-mail]

Received 16 October 1992

Machines

We consider the problem of mechanically constructing abstract machines from operational semantics, producing intermediate-level specications 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 specications have the form of abstract machines. Though not automatable in general, this approach to constructing machine implementations can be mechanized, providing machine-veried correctness proofs. As examples we present the transformation of specications 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 specication and the correctness of the transformations applied.

1. Introduction

The correctness of programming language implementations is an important issue con- fronting language designers and implementors. Traditionally, such implementations are rst built “by hand” and only then proved correct. Unfortunately, the resulting imple- mentations may have little relationship to the language’s semantic specications and so correctness may be dicult to show. For realistic languages, such correctness proofs become unwieldy because of the overwhelming amount of implementation-level informa- tion that must be correlated. In an alternative approach, a language implementation is constructedfromthe semantic specication in such a way that the resulting imple- mentation is guaranteed to satisfy correctness requirements: no independent proof being necessary. This approach may provide a mechanical, if not automatic, process allowing the correctness to be machine checked. This latter point is important when considering