Extensional embedding of a strongly stable model of PCF

Abstract

This work takes place in denotational semantics of simply typed functional programming languages (like PCF, see [8]). We describe a general method for performing simultaneously an extensional and a “stable” semantics in such a way that only maps existing in both semantics subsist in our model. The construction is carried out in the framework of strongly stable functions that we have recently defined and which is a refinement of stable semantics such that, at first order, all functions are sequential. However we do not use any peculiar feature of this semantics and constructions presented here could just as well be carried out in the more usual stable framework.