dc.contributor.advisor Plotkin, Gordon en dc.contributor.advisor Power, John en dc.contributor.author Denney, Ewen WKC en dc.date.accessioned 2004-03-02T15:59:29Z dc.date.available 2004-03-02T15:59:29Z dc.date.issued 1999-07 dc.identifier.uri http://hdl.handle.net/1842/381 dc.description.abstract We give a canonical program refinement calculus based on the lambda calculus and classical first-order predicate logic, and study its proof theory and semantics. The intention is to construct a metalanguage for refinement in which basic principles of program development can be studied. en The idea is that it should be possible to induce a refinement calculus in a generic manner from a programming language and a program logic. For concreteness, we adopt the simply-typed lambda calculus augmented with primitive recursion as a paradigmatic typed functional programming language, and use classical first-order logic as a simple program logic. A key feature is the construction of the refinement calculus in a modular fashion, as the combination of two orthogonal extensions to the underlying programming language (in this case, the simply-typed lambda calculus). The crucial observation is that a refinement calculus is given by extending a programming language to allow indeterminate expressions (or 'stubs') involving the construction 'some program x such that P'. Factoring this into 'some x ...' and '... such that P', we first study extensions to the lambda calculus providing separate analyses of what we might call 'true' stubs, and structured specifications. The questions we are concerned with in these calculi are how do stubs interact with the programming language, and what is a suitable notion of structured specification for program development. The full refinement calculus is then constructed in a natural way as the combination of these two subcalculi. The claim that the subcalculi are orthogonal extensions to the lambda calculus is justified by a result that a refinement can actually be factored into simpler judgements in the subcalculi, that is, into logical reasoning and simple decomposition. The semantics for the calculi are given using Henkin models with additional structure. Both simply-typed lambda calculus and first-order logic are interpreted using Henkin models themselves. The two subcalculi require some extra structure and the full refinement calculus is modelled by Henkin models with a combination of these extra requirements. There are soundness and completeness results for each calculus, and by virtue of there being certain embeddings of models we can infer that the refinement calculus is a conservative extension of both of the subcalculi which, in turn, are conservative extensions of the lambda calculus. dc.contributor.sponsor Engineering and Physical Sciences Research Council (EPSRC) en dc.format.extent 802264 bytes en dc.format.extent 1275675 bytes en dc.format.extent 1433547 bytes en dc.format.mimetype application/x-dvi en dc.format.mimetype application/pdf en dc.format.mimetype application/postscript en dc.language.iso en dc.publisher University of Edinburgh. College of Science and Engineering. School of Informatics. en dc.title A Theory of Program Refinement en dc.type Thesis or Dissertation en dc.type.qualificationlevel Doctoral en dc.type.qualificationname PhD Doctor of Philosophy en
﻿