Show simple item record

dc.contributor.advisorPlotkin, Gordonen
dc.contributor.advisorPower, Johnen
dc.contributor.authorDenney, Ewen WKCen
dc.date.accessioned2004-03-02T15:59:29Z
dc.date.available2004-03-02T15:59:29Z
dc.date.issued1999-07
dc.identifier.urihttp://hdl.handle.net/1842/381
dc.description.abstractWe 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. 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.en
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.format.extent802264 bytesen
dc.format.extent1275675 bytesen
dc.format.extent1433547 bytesen
dc.format.mimetypeapplication/x-dvien
dc.format.mimetypeapplication/pdfen
dc.format.mimetypeapplication/postscripten
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.titleA Theory of Program Refinementen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record