Formalising generalised substitutions
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]
|Collections||ANU Research Publications|
|01_Dawson_Formalising_generalised_2007.pdf||126.79 kB||Adobe PDF||Request a copy|
|02_Dawson_Formalising_generalised_2007.pdf||73.59 kB||Adobe PDF||Request a copy|
|03_Dawson_Formalising_generalised_2007.pdf||369.22 kB||Adobe PDF||Request a copy|
|04_Dawson_Formalising_generalised_2007.pdf||21.56 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.