{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:52:24Z","timestamp":1694623944796},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[1995,11,1]],"date-time":"1995-11-01T00:00:00Z","timestamp":815184000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Using 2-categorical laws of algorithmic refinement, we show soundness of data refinement for stored programs and hence for higher order procedures with value\/result parameters. The refinement laws hold in a model that slightly generalizes the standard predicate transformer semantics for the usual imperative programming constructs including prescriptions.<\/jats:p>","DOI":"10.1007\/bf01210999","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T12:43:49Z","timestamp":1109335429000},"page":"652-662","source":"Crossref","is-referenced-by-count":7,"title":["Data refinement, call by value and higher order programs"],"prefix":"10.1145","volume":"7","author":[{"given":"David A.","family":"Naumann","sequence":"first","affiliation":[{"name":"Mathematics and Computer Science, Southwestern University, PO Box 770, 78627, Georgetown, Texas, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90065-T"},{"key":"e_1_2_1_2_2_2","unstructured":"Back R.J.R.: Correctness preserving program refinements: Proof theory and applications. Technical Report Tract 131 CWI 1980."},{"key":"e_1_2_1_2_3_2","unstructured":"Back R.J.R. and Butler M.J.: Exploring summation and product operators in the refinement calculus. Technical Report on Computer Science & Mathematics Ser. A No. 152 Abo Akademi September 1994. Available from ftp:\/\/ftp.abo.fi\/pub\/cs\/techreports\/reports\/A94-152.ps.Z."},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bonsangue M. and Kok J. N.: Isomorphisms between predicate and state transformers. In MFCS pages 301\u2013310. Springer LNCS 711 1993.","DOI":"10.1007\/3-540-57182-5_22"},{"key":"e_1_2_1_2_5_2","first-page":"931","article-title":"On local adjointness of distributive bicategories","volume":"7","author":"Betti R.","year":"1988","journal-title":"Bolletino U.M.I."},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Chen W. and Udding J.T.: Towards a calculus of data refinement. In Proceedings Mathematics of Program Construction pages 197\u2013218 1989. LNCS 375.","DOI":"10.1007\/3-540-51305-1_11"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90001-C"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90029-2"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)90006-X"},{"key":"e_1_2_1_2_10_2","unstructured":"Hoare C.A.R. and He J.: Data refinement in a categorical setting. Technical Monograph PRG-PRG-90 November 1990."},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_2_12_2","unstructured":"Kelly G.M.: Basic Concepts of Enriched Category Theory volume 64 of London Mathematical Society Lecture Notes . Cambridge 1982."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Kinoshita Y. and Power J.: Enriched categories and data refinement. Technical Report 94-23 University of Edinburgh Department of Computer Science 1994.","DOI":"10.1017\/CBO9780511554629.004"},{"key":"e_1_2_1_2_14_2","unstructured":"Martin C.E.: Preordered categories and predicate transformers. Dissertation Oxford University 1991."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Mitchell J.C.: Type systems for programming languages. In J. van Leeuwen editor Handbook of Theoretical Computer Science pages 365\u2013458. MIT Press\/Elsevier 1990.","DOI":"10.1016\/B978-0-444-88074-1.50013-5"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/69304.69305"},{"key":"e_1_2_1_2_17_2","unstructured":"Morgan C.: Programming from Specifications second edition . Prentice Hall 1994."},{"key":"e_1_2_1_2_18_2","unstructured":"Naumann D.A.: Predicate transformers and higher order programs. Theoretical Computer Science 1992. To appear."},{"key":"e_1_2_1_2_19_2","volume-title":"Dissertation","author":"Naumann D.A.","year":"1992"},{"key":"e_1_2_1_2_20_2","unstructured":"Naumann D.A.: Categorical models of higher order imperative programming. Typescript 1994."},{"key":"e_1_2_1_2_21_2","unstructured":"Naumann D.A.: Predicate transformer semantics of an Oberon-like language. In ErnstR\u00fcdiger Olderog editor Programming Concepts Methods and Calculi IFIP Transactions A-56. Elsevier 1994."},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)00049-2"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"O'Hearn P.W. and Tennant R.D.: Relational parametricity and local variables (preliminary report). In Proceedings Twentieth POPL pages 171\u2013184 1993.","DOI":"10.1145\/158511.158624"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Pierce B.C.: Basic Category Theory for Computer Scientists . MIT 1991.","DOI":"10.7551\/mitpress\/1524.001.0001"},{"key":"e_1_2_1_2_25_2","unstructured":"Plotkin G.: Post-graduate lecture notes in advanced domain theory. Typescript 1981."},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Power A.J.: An algebraic formulation for data refinement. In Proceedings 5th International Conf. on Mathematical Foundations of Programming Semantics pages 390\u2013401 1989. LNCS 442.","DOI":"10.1007\/BFb0040270"},{"key":"e_1_2_1_2_27_2","unstructured":"Smyth M.B.: Power domains and predicate transformers: A topological view. In ICALP 1983. LNCS 154."},{"key":"e_1_2_1_2_28_2","unstructured":"Tennant R.D.: Correctness of data representations in Algol-like languages. In A.W. Roscoe editor A Classical Mind: Essays Dedicated to C.A.R. Hoare . Prentice-Hall 1994."},{"key":"e_1_2_1_2_29_2","unstructured":"Vickers S.: Topology Via Logic . Cambridge 1989."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01210999.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01210999\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01210999","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:24:46Z","timestamp":1641482686000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01210999"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,11]]},"references-count":29,"journal-issue":{"issue":"6","published-print":{"date-parts":[[1995,11]]}},"alternative-id":["10.1007\/BF01210999"],"URL":"https:\/\/doi.org\/10.1007\/bf01210999","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,11]]}}}