Show simple item record

dc.contributor.advisorGilmore, Stephenen
dc.contributor.advisorAnderson, Stuarten
dc.contributor.authorOwens, Christopheren
dc.date.accessioned2004-03-02T15:51:48Z
dc.date.available2004-03-02T15:51:48Z
dc.date.issued1999-07
dc.identifier.urihttp://hdl.handle.net/1842/380
dc.description.abstractOne reason for studying and programming in functional programming languages is that they are easy to reason about, yet there is surprisingly little work on proving the correctness of large functional programs. In this dissertation I show how to provide a system for proving the correctness of large programs written in a major functional programming language, ML. ML is split into two parts: the Core (in which the actual programs are written), and Modules (which are used to structure Core programs). The dissertation has three main themes: Due to the detail and complexity of proofs of programs, a realistic system should use a computer proof assistant, and so I first discuss how such a system can be coded in a generic proof assistant (I use Paulson's Isabelle). I give a formal proof system for proving properties of programs written in the functional part of Core ML. The Modules language is one of ML's strengths: it allows the programmer to write large programs by controlling the interactions between its parts. In the final part of the dissertation I give a method of proving correctness of ML Modules programs using the well-known data reification method. Proofs of reification using this method boil down to proofs in the system for the Core.en
dc.format.extent498780 bytesen
dc.format.extent1135468 bytesen
dc.format.extent902840 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.titleProving Correctness of Modular Functional Programsen
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