Abstract
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 about generalised substitutions follow from the model of computation which we describe.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. CUP, Cambridge (1996)
Barr, M., Wells, C.: Toposes, Triples and Theories. Springer, Heidelberg (1983), http://www.cwru.edu/artsci/math/wells/pub/ttt.html
Chartier, P.: Formalisation of B in Isabelle/HOL. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 66–83. Springer, Heidelberg (1998)
Dawson, J.E.: Compound Monads and the Kleisli Category (unpublished note), http://users.rsise.anu.edu.au/~jeremy/pubs/cmkc/
Dawson, J.E.: Isabelle files, http://users.rsise.anu.edu.au/~jeremy/isabelle/fgc/
Dawson, J.E.: Formalising General Correctness. In: ENTCS. Computing: The Australasian Theory Symposium, vol. 91, pp. 21–42 (2004), http://www.elsevier.com/locate/entcs
Dunne, S.: Abstract Commands: A Uniform Notation for Specifications and Implementations. In: ENTCS. Computing: The Australasian Theory Symposium, vol. 42, pp. 104–123 (2001), http://www.elsevier.com/locate/entcs
Dunne, S.: A Theory of Generalised Substitutions. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 270–290. Springer, Heidelberg (2002)
Jones, M.P., Duponcheel, L.: Composing Monads. Research Report YALEU/DCS/RR-1004, Yale University (December 1993)
Wadler, P.: The Essence of Functional Programming. In: POPL1992. Symposium on Principles of Programming Languages, pp. 1–14 (1992)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dawson, J.E. (2007). Formalising Generalised Substitutions. In: Schneider, K., Brandt, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2007. Lecture Notes in Computer Science, vol 4732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74591-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-74591-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74590-7
Online ISBN: 978-3-540-74591-4
eBook Packages: Computer ScienceComputer Science (R0)