{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:13:44Z","timestamp":1725455624767},"publisher-location":"Berlin\/Heidelberg","reference-count":13,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540557075"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0023877","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T06:02:35Z","timestamp":1132380155000},"page":"229-240","source":"Crossref","is-referenced-by-count":0,"title":["A categorical interpretation of partial function logic and Hoare logic"],"prefix":"10.1007","author":[{"given":"P. M. W.","family":"Knijnenburg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F.","family":"Nordemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K.R. Apt","year":"1981","unstructured":"K.R. Apt. Ten years of Hoare's logic. ACM Trans. on Prog. Lan. and Syst., 3:431\u2013483, 1981.","journal-title":"ACM Trans. on Prog. Lan. and Syst."},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"M.J. Beeson. Proving programs and programming proofs. In B. Marcus et al., editor, Logic, Methodology and Philosophy of Science VII. Elsevier, 1986.","DOI":"10.1016\/S0049-237X(09)70684-6"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"P. Cousot. Methods and logics for proving programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Elsevier, 1990. Vol. B.","DOI":"10.1016\/B978-0-444-88074-1.50020-2"},{"key":"20_CR4","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1017\/S0305004100057534","volume":"88","author":"J.M.E. Hyland","year":"1980","unstructured":"J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts. Tripos theory. Math. Proc. Camb. Phil. Soc., 88:205\u2013232, 1980.","journal-title":"Math. Proc. Camb. Phil. Soc."},{"issue":"10","key":"20_CR5","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"C.A.R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(10):576\u2013580, 1969.","journal-title":"Comm. ACM"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"F.W. Lawvere. Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In A. Heller, editor, Proc. New York Symp. on Applications of Categorical Algebra, pages 1\u201314. Amer. Math. Soc., 1970.","DOI":"10.1090\/pspum\/017\/0257175"},{"key":"20_CR7","unstructured":"A.M. Pitts. Notes on categorical logic. Technical report, Computer Laboratory, Univ. of Cambridge, 1989."},{"key":"20_CR8","unstructured":"G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, Univ. of Oxford, 1986."},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90034-X","volume":"79","author":"E. Robinson","year":"1988","unstructured":"E. Robinson and G. Rosolini. Categories of partial maps. Information and Computation, 79:95\u2013130, 1988.","journal-title":"Information and Computation"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"D.S. Scott. Identity and existence in intuitionistic logic. In M.P. Fourman, C.J. Mulvey, and D.S. Scott, editors, Applications of Sheaves, 1979.","DOI":"10.1007\/BFb0061839"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1016\/0020-0190(87)90158-X","volume":"24","author":"R.D. Tennent","year":"1987","unstructured":"R.D. Tennent. A note on undefined expression values in programming logics. Inf. Proc. Letters, 24:331\u2013333, 1987.","journal-title":"Inf. Proc. Letters"},{"key":"20_CR12","unstructured":"D. van Dalen and A.S. Troelstra. Constructivism in Mathematics, volume I. North Holland, 1988."},{"key":"20_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(87)90025-9","volume":"53","author":"E.G Wagner","year":"1987","unstructured":"E.G Wagner. A categorical treatment of pre-and post-conditions. Theor. Comp. Sc., 53:3\u201324, 1987.","journal-title":"Theor. Comp. Sc."}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science \u2014 Tver '92"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0023877.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:51:00Z","timestamp":1607550660000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0023877"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540557075"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0023877","relation":{},"subject":[]}}