Show simple item record

dc.contributor.authorCohn, Avra Jeanen
dc.date.accessioned2013-04-05T11:17:01Z
dc.date.available2013-04-05T11:17:01Z
dc.date.issued1979
dc.identifier.urihttp://hdl.handle.net/1842/6643
dc.description.abstractThree studies in the machine assisted proof of recursion implementation are described. The verification system used is Edinburgh LCF (Logic for Computable Functions). Proofs are generated, in LCF, in a goal-oriented fashion by the application of strategies reflecting informal proof plans. LCF is introduced in Chapter 1. We present three case studies in which proof strategies are developed and (except in the third) tested in LCF. Chapter 2 contains an account of the machine generated proofs of three program transformations (from recursive to iterative function schemata). Two of the examples are taken from Manna and Waldinger. In each case, the recursion is implemented by the introduction of a new data type, e.g., a stack or counter. Some progress is made towards the development of a general strategy for producing the equivalence proofs of recursive and iterative function schemata by machine. Chapter 3 is concerned with the machine generated proof of the correctness of a compiling algorithm. The formulation, borrowed from Russell, includes a simple imperative language with a while and conditional construct, and a low level language of labelled statements, including jumps. We have, in LCF, formalised his denotational descriptions of the two languages and performed a proof of the preservation of the semantics under compilation. In Chapter 4, we express and informally prove the correctness of a compiling algorithm for a language containing declarations and calls of recursive procedures. We present a low level language whose semantics model a standard activation stack implementation. Certain theoretical difficulties (connected with recursively defined relations) are discussed, and a proposed proof in LCF is outlined. The emphasis in this work is less on proving original theorems, or even automatically finding proofs of known theorems, than on (i) exhibiting and analysing the underlying structure of proofs, and of machine proof attempts, and (ii) investigating the nature of the interaction (between a user and a computer system) required to generate proofs mechanically; that is, the transition from informal proof plans to behaviours which cause formal proofs to be performed.en
dc.language.isoen
dc.publisherThe University of Edinburghen
dc.relation.hasversionA. J. Cohn, High Level Proof in LCF, Proceedings, Fourth Workshop on Automated Deduction, Austin, Texas, Feb. 1-3, 1979, and also as EUCSD Internal Report CSR-35-78, Nov. 1978en
dc.subjectEdinburgh LCF (Computer system).en
dc.subjectComputer programsen
dc.subjecttestingen
dc.subjectmachine generated proofsen
dc.subjectstructure of proofsen
dc.titleMachine Assisted Proofs of Recursion Implementationen
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