Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >

Please use this identifier to cite or link to this item:

This item has been viewed 4 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
ECS-LFCS-98-390.dviLaTeX DVI File394.96 kBTeX dviView/Open
ECS-LFCS-98-390.pdfAdobe PDF1.01 MBAdobe PDFView/Open
ECS-LFCS-98-390.psPostScript File760.98 kBPostscriptView/Open
Title: Applicative Notions in ML-like Programs
Authors: Ling, Budi H
Supervisor(s): Fourman, Michael
Anderson, Stuart
Issue Date: Jul-1998
Publisher: University of Edinburgh. College of Science and Engineering. School of Informatics.
Abstract: Pure functional languages are expressive tools for writing modular and reliable code. State in programming languages is a useful tool for programming dynamic systems. However, their combination yields programming languages that are difficult to model and to reason about. There have been ongoing attempts to find subsets of the whole languages which have good properties; in particular subsets where the programs are more modular and the side effects are controlled. The existing studies are: interference control, typing with side-effects information, and linear logic based languages. This thesis presents a new classification for a paradigm called constant program throughout a computational invariant. A program is called constant throughout an invariant R if its input-output behaviour is constant over any variations of state that satisfy the invariant R. Hence such a program behaves in an applicative way when it is executed in a context that satisfies the invariant R. The language of discussion is a pure ML fragment augmented with ref, :=, and !. Programs with side effects are modelled in terms of sets, functions, and the side effect monad. Computational invariants are modelled in terms of transition systems. The notion of being constant throughout an invariant requires the notion of indistinguishability throughout an invariant and we define the latter using logical relation technique. We give two definitions of each of them: the first one can be used for reasoning about programs with at stores adequately. The second one is more sensitive to the behaviour of ref and gives a better account of constant programs with dynamic allocations. Our results are: indistinguishability throughout an invariant R is an equivalence relation over elements that are constant throughout R, and the notion of being constant throughout an invariant is preserved under function application. On the practical side we present some substantial ML examples which use references and side effects but externally behave in a constant way, together with the proofs that they are classified as being constant. These are evidences that our notions are useful concepts in the practise of writing modular programs.
Appears in Collections:Informatics thesis and dissertation collection

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.


Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy