Article contents
An application of PER models to program extraction
Published online by Cambridge University Press: 04 March 2009
Abstract
Type theory allows us to extract from a constructive proof that a specification is satisfiable a program that satisfies the specification. Algorithms for optimization of such programs are currently the object of research.
In this paper we consider one such algorithm, which was described in Beeson (1985) and which we will call ‘Harrop’. This algorithm greatly simplifies programs extracted from proofs in the Pure Construction Calculus. We use a Partial Equivalence Relation model for higher order lambda calculus, to check that t and Harrop(t) return the same outputs from the same inputs, i.e. that they are extensionally equal.
As a corollary, we show that it is correct (and, of course, useful) to replace a program t with Harrop(t). Such a correctness result has already been proved by Möhring (Möhring 1989a, 1989b) using realizability semantics, but we obtain it as a corollary of a new result, the extensional equality between t and Harrop(t). Also the semantic method we use is interesting in its own right.
- Type
- Research Article
- Information
- Copyright
- Copyright © Cambridge University Press 1993
References
- 3
- Cited by