Skip navigation
Skip navigation

Formalising generalised substitutions

Dawson, Jeremy


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


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:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator