Proving the correctness of storage representations
- 1 January 1992
- proceedings article
- Published by Association for Computing Machinery (ACM)
- No. 1,p. 151-160
- https://doi.org/10.1145/141471.141528
Abstract
Conventional techniques for semantics-directed compiler derivation yield abstract machines that manipulate trees. However, in order to produce a real compiler, one has to represent these trees in memory. In this paper we show how the technique of storage-layout relations can be applied to verify the correctness of storage representations in a very general way. This technique allows us to separate denotational from operational reasoning, so that each can be used when needed. As an example, we show the correctness of a stack implementation of a language including dynamic catch and throw. The representation uses static and dynamic links to thread the environment and continuation through the stack. We discuss other uses of these techniques.Keywords
This publication has 8 references indexed in Scilit:
- Tag-free garbage collection for strongly typed programming languagesPublished by Association for Computing Machinery (ACM) ,1991
- Runtime tags aren't necessaryHigher-Order and Symbolic Computation, 1989
- A simple applicative language: mini-MLPublished by Association for Computing Machinery (ACM) ,1986
- The global storage needs of a subcomputationPublished by Association for Computing Machinery (ACM) ,1984
- The scheme 311 compiler an exercise in denotational semanticsPublished by Association for Computing Machinery (ACM) ,1984
- Loops in combinator-based compilersInformation and Control, 1983
- Semantics-directed machine architecturePublished by Association for Computing Machinery (ACM) ,1982
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975