Specifying the correctness of binding-time analysis
- 1 July 1993
- journal article
- research article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 3 (3) , 365-387
- https://doi.org/10.1017/s0956796800000782
Abstract
Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conventional properties of partial evaluators, such as the Futamura projections, are consequences of this specification. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for incorporating flow analyses into verified compilers.Keywords
This publication has 14 references indexed in Scilit:
- A self-applicable partial evaluator for the lambda calculusACM Transactions on Programming Languages and Systems, 1992
- Proving the correctness of storage representationsACM SIGPLAN Lisp Pointers, 1992
- Theoretical Pearls: Self-interpretation in lambda calculusJournal of Functional Programming, 1991
- A strongly-typed self-applicable partial evaluatorPublished by Springer Nature ,1991
- Efficient type inference for higher-order binding-time analysisPublished by Springer Nature ,1991
- Binding time analysis for high order untyped functional languagesPublished by Association for Computing Machinery (ACM) ,1990
- Two-level semantics and code generationTheoretical Computer Science, 1988
- Higher-order abstract syntaxPublished by Association for Computing Machinery (ACM) ,1988
- The scheme 311 compiler an exercise in denotational semanticsPublished by Association for Computing Machinery (ACM) ,1984
- Deriving Target Code as a Representation of Continuation SemanticsACM Transactions on Programming Languages and Systems, 1982