Deriving Denotational Semantics from Axiomatic Semantics within Constructive Set Theory

In this paper we provide a constructive interpretation of Hoare logics with the constructive and intensional theory of program development TK. As a result it becomes possible to derive denotational semantics from axiomatic semantics; this facilitates a re-appraisal of the relationship between a programming language, its standard model and its theory of program properties and holds out the prospect for a more general analysis of formal methods from a constructive perspective. 2 Introduction Much recent research in software science has been devoted to the investigation of program derivation in some constructive framework ([Bac 89], [Con 86], [HaN 87], [Hen 89] and [Moh 85] are examples which utilise Martin-Lof's Type Theory [Mar 82], Feferman's T 0 [Fef 79], Henson and Turner's TK [HeT 88] and Huet & Coquand's Theory of Constructions [HuC 85]). It is our belief that, more generally, a constructive foundation for software science is both philosophically appropriate to, and potentially ..