{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:58Z","timestamp":1725663838148},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540571827"},{"type":"electronic","value":"9783540479277"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-57182-5_22","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:09:36Z","timestamp":1330258176000},"page":"301-310","source":"Crossref","is-referenced-by-count":6,"title":["Isomorphisms between predicate and state transformers"],"prefix":"10.1007","author":[{"given":"Marcello","family":"Bonsangue","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost N.","family":"Kok","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1006\/inco.1991.9999","volume":"92","author":"S. Abramsky","year":"1991","unstructured":"S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161\u2013218, 1991.","journal-title":"Information and Computation"},{"issue":"4","key":"22_CR2","doi-asserted-by":"crossref","first-page":"724","DOI":"10.1145\/6490.6494","volume":"33","author":"K. R. Apt","year":"1986","unstructured":"K. R. Apt and G. Plotkin. Countable nondeterminism and random assignment. Journal of the ACM, 33(4):724\u2013767, October 1986.","journal-title":"Journal of the ACM"},{"key":"22_CR3","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters, 21:181\u2013185, 1985.","journal-title":"Information Processing Letters"},{"key":"22_CR4","volume-title":"volume 131 of Mathematical Centre Tracts","author":"R.-J. R. R. Back","year":"1980","unstructured":"R.-J.R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Centre Tracts. Mathematical Centre, Amsterdam, 1980."},{"key":"22_CR5","unstructured":"J. W. de Bakker. Mathematical Theory of Program Corretness. Prentice-Hall, 1980."},{"key":"22_CR6","volume-title":"Technical Report CS-R9267","author":"M. Bonsangue","year":"1992","unstructured":"M. Bonsangue and J. N. Kok. Semantics, orderings and recursion in the weakest precondition calculus. Technical Report CS-R9267, Centre for Mathematics and Computer Science, Amsterdam, 1992. Extended abstract to appear in the proceedings of the Rex Workshop '92 'semantics: Foundations and Applications\u2019 LNCS 666, 1993."},{"key":"22_CR7","volume-title":"Technical report","author":"M. Bonsangue","year":"1993","unstructured":"M. Bonsangue and J. N. Kok. Isomorphisms between state and predicate transformers. Technical report, Centre for Mathematics and Computer Science, Amsterdam, 1993. Available through anonymous ftp from ftp.cwi.nl."},{"key":"22_CR8","unstructured":"F. van Breugel. Relating state transformation semantics and predicate transformer semantics for parallel programs. To appear, 1993."},{"key":"22_CR9","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"22_CR10","unstructured":"R. Engelking. General Topology. Polish Scientific Publishers, 1977."},{"key":"22_CR11","unstructured":"P. Hitchcock and D. Park. Induction rules and termination proofs. In International Conference on Automata, Languages and Programming, 1972."},{"key":"22_CR12","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1016\/0890-5401(87)90021-6","volume":"74","author":"K. Hrbacek","year":"1987","unstructured":"K. Hrbacek. Convex Powerdomains I. Information and computation, 74:198\u2013225, 1987.","journal-title":"Information and computation"},{"key":"22_CR13","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1016\/0890-5401(89)90034-5","volume":"81","author":"K. Hrbacek","year":"1989","unstructured":"K. Hrbacek. Convex Powerdomains II. Information and computation, 81:290\u2013317, 1989.","journal-title":"Information and computation"},{"key":"22_CR14","unstructured":"M.Z. Kwiatowska. On topological characterization of behavioural properties. In G.M. Reed, A.W. Roscoe, and R.F. Wachter, editors, Topology and Category Theory in Computer Sciences \u2014 Proc. Oxford Topology Symposioum, June 1989, pages 153\u2013177. Oxford Science Pubblications, 1991."},{"key":"22_CR15","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"L. Lamport. Proving the correctness of a multiprocess programs. IEEE Transaction on Software Eng., SE-3:125\u2013143, 1977.","journal-title":"IEEE Transaction on Software Eng."},{"issue":"2","key":"22_CR16","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1145\/322123.322134","volume":"26","author":"G. Milne","year":"1979","unstructured":"G. Milne and R. Milner. Concurrent processes and their syntax. J. ACM, 26, 2:302\u2013321, 1979.","journal-title":"J. ACM"},{"key":"22_CR17","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11-4","author":"G. Nelson","year":"1989","unstructured":"G. Nelson. A generalization of Dijkstra's calculus. ACM Transaction on Programming Languages and Systems, 11-4:517\u2013561, 1989.","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"22_CR18","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1137\/0205035","volume":"5","author":"G. D. Plotkin","year":"1976","unstructured":"G. D. Plotkin. A powerdomain construction. SIAM J. Comput., 5:452\u2013487, 1976.","journal-title":"SIAM J. Comput."},{"key":"22_CR19","first-page":"527","volume-title":"volume 86 of Lecture Notes in Computer Science","author":"G. D. Plotkin","year":"1979","unstructured":"G. D. Plotkin. Dijkstra's predicate transformer and Smyth's powerdomain. In Proceedings of the Winter School on Abstract Software Specification, volume 86 of Lecture Notes in Computer Science, pages 527\u2013553. Springer-Verlag, Berlin, 1979."},{"key":"22_CR20","unstructured":"G.D. Plotkin. Post-graduate lecture notes in advanced domain theory (incorporating the \u201cPisa Notes\u201d). Department of Computer Science, Univ. of Edinburgh, 1981."},{"key":"22_CR21","series-title":"volume 45 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1007\/3-540-07854-1_217","volume-title":"Mathematical foundations of computer science","author":"W. P. Roever de","year":"1976","unstructured":"W.P. de Roever. Dijkstra's predicate transformer, non-determinism, recursion, and terminations. In Mathematical foundations of computer science, volume 45 of Lecture Notes in Computer Science, pages 472\u2013481. Springer-Verlag, Berlin, 1976."},{"issue":"1","key":"22_CR22","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0022-0000(78)90048-X","volume":"16","author":"M. B. Smyth","year":"1978","unstructured":"M.B. Smyth. Power domains. J. Comput. Syst. Sci., 16,1:23\u201336, 1978.","journal-title":"J. Comput. Syst. Sci."},{"key":"22_CR23","series-title":"volume 154 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/BFb0036946","volume-title":"Proceedings of ICALP '83 (Barcelona)","author":"M. B. Smyth","year":"1983","unstructured":"M.B. Smyth. Power domains and predicate transformers: A topological view. In Proceedings of ICALP '83 (Barcelona), volume 154 of Lecture Notes in Computer Science, pages 662\u2013675. Springer-Verlag, Berlin, 1983."},{"key":"22_CR24","unstructured":"M.B. Smyth. Topology. In S. Abramsky, D.M. Gabbay, and T.S.E. Malbaum, editors, Handbook of Logic in Computer Science, volume I \u2014 Background: Mathematical Structures. Oxford University Press, 1992."},{"key":"22_CR25","unstructured":"J. von Wright. A Lattice-theoretical Basis for Program Refinement. PhD thesis, Abo Akademi, 1990."}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1993"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57182-5_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T00:59:29Z","timestamp":1619571569000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57182-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540571827","9783540479277"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-57182-5_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}