@inproceedings{462224aa8c11465b878a7118d095ac5f,
title = "Formalising generalised substitutions",
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.",
keywords = "General correctness, Generalised substitution",
author = "Dawson, {Jeremy E.}",
year = "2007",
doi = "10.1007/978-3-540-74591-4_6",
language = "English",
isbn = "9783540745907",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "54--69",
booktitle = "Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings",
address = "Germany",
note = "20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007 ; Conference date: 10-09-2007 Through 13-09-2007",
}