@inproceedings{crole1993factoring,
author = {Crole, Roy L. and Gordon, Andy},
title = {Factoring an Adequacy Proof (Preliminary Report)},
booktitle = {Proceedings of the 1993 Glasgow Workshop on Functional Programming, Ayr, Scotland, 5-7 July 1993},
year = {1993},
month = {July},
abstract = {This paper contributes to the methodology of using metalogics for reasoning about programming languages. As a concrete example we consider a fragment of ML corresponding to call-by-value PCF and translate it into a metalogic which contains (amongst other types) computation types and a fixpoint type. The main result is a soundness property (*): if the denotations of two programs are provably equal in the metalogic, they have the same operationally observable behaviour. As usual, this follows from a computational adequacy result. In early notes, Plotkin showed how such proofs could be factored into two stages, the first non-trivial and the second (essentially) routine; our contribution is to rework his suggestion within a new framework. We define a metalogic, which incorporates computation and fixpoint types, and specify a modular translation of the ML fragment. Our proof of (*) factors into two parts. First, the term language of the metalogic is equipped with an operational semantics and a (generic) computational adequacy result obtained. Second, a simple syntactic argument establishes a correspondence between the operational behaviour of an object program and of its denotation. The first part is not routine but is proved once and for all. The second is a detailed but essentially trivial calculation that is easily adaptable to other object languages. Such a factored proof is important because it promises to scale up more easily than a monolithic one. We show that it may be adapted to an object language with call-by-name functions and one with a simple exception mechanism.},
publisher = {Springer London},
url = {http://approjects.co.za/?big=en-us/research/publication/factoring-adequacy-proof-preliminary-report/},
pages = {9-25},
isbn = {978-3-540-19879-6 (Print) 978-1-4471-3236-3 (Online)},
edition = {Proceedings of the 1993 Glasgow Workshop on Functional Programming, Ayr, Scotland, 5–7 July 1993},
}