Skip navigation
Skip navigation

Formalising generalised substitutions

Dawson, Jeremy

Description

We use the theorem prover Isabelle to formalise and machine-check results of the theory of generalised substitutions given by Dunne and used in the B method. We describe the model of computation implicit in this theory and show how this is based on a compound monad, and we contrast this model of computation and monad with those implicit in Dunne's theory of abstract commands. Subject to a qualification concerning frames, we prove, using the Isabelle/HOL theorem prover, that Dunne's results...[Show more]

CollectionsANU Research Publications
Date published: 2007
Type: Book chapter
URI: http://hdl.handle.net/1885/39514

Download

File Description SizeFormat Image
01_Dawson_Formalising_generalised_2007.pdf126.79 kBAdobe PDF    Request a copy
02_Dawson_Formalising_generalised_2007.pdf73.59 kBAdobe PDF    Request a copy
03_Dawson_Formalising_generalised_2007.pdf369.22 kBAdobe PDF    Request a copy
04_Dawson_Formalising_generalised_2007.pdf21.56 kBAdobe PDF    Request a copy


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

Updated:  23 August 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator