{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:55Z","timestamp":1761611215551},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665366"},{"type":"electronic","value":"9783540481683"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48168-0_39","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T06:30:26Z","timestamp":1196490626000},"page":"562-576","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Data-Refinement for Call-By-Value Programming Languages"],"prefix":"10.1007","author":[{"given":"Yoshiki","family":"Kinoshita","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Power","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"unstructured":"Fiore, M., Plotkin, G.D.: An axiomatisation of computationally adequate domain-theoretic models of FPC. Proc LICS 94. IEEE Press (1994) 92\u2013102.","key":"39_CR1"},{"key":"39_CR2","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/BF01212407","volume":"5","author":"P.H.B. Gardiner","year":"1993","unstructured":"Gardiner, P.H.B., Morgan, C.:A single complete rule for data refinement. Formal Aspects of Computing 5 (1993) 367\u2013382.","journal-title":"Formal Aspects of Computing"},{"doi-asserted-by":"crossref","unstructured":"Hermida, C.A.: Fibrations, Logical Predicates and Indeterminates. Ph.D. thesis. Edinburgh (1993) available as ECS-LFCS-93-277.","key":"39_CR3","DOI":"10.7146\/dpb.v22i462.6935"},{"key":"39_CR4","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1 (1972) 271\u2013281.","journal-title":"Acta Informatica"},{"unstructured":"Hoare, C.A.R.: Data refinement in a categorical setting. (1987) (draft).","key":"39_CR5"},{"unstructured":"Hoare, C.A.R., Jifeng, H.: Data refinement in a categorical setting. (1990) (draft).","key":"39_CR6"},{"unstructured":"Honsell, F., Sannella, D.T.: Pre-logical relations. Proc. CSL 99 (in this volume).","key":"39_CR7"},{"unstructured":"Johnstone, P.T., Power, A.J., Tsujishita, T., Watanabe, H., Worrell, J.: An Axiomatics for Categories of Transition Systems as Coalgebras. Proc LICS 98. IEEE Press (1998) 207\u2013213.","key":"39_CR8"},{"unstructured":"Kelly, G.M.: Basic concepts of enriched category theory. Cambridge University Press (1982).","key":"39_CR9"},{"key":"39_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BFb0014552","volume-title":"Proc TACS 97","author":"Y. Kinoshita","year":"1997","unstructured":"Kinoshita, Y., O\u2019Hearn, P., Power, A.J., Takeyama, M., Tennent, R.D.: An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement. Proc TACS 97. LNCS 1281. Abadi and Ito (eds.) Springer (1997) 191\u2013212."},{"unstructured":"Kinoshita, Y., Power, A.J.: Data refinement and algebraic structure. Acta Informatica (to appear).","key":"39_CR11"},{"unstructured":"Kinoshita, Y., Power, A.J., Takeyama, M.: Sketches. J. Pure Appl. Algebra (to appear).","key":"39_CR12"},{"unstructured":"Kinoshita, Y., Power, A.J., Watanabe, H.: A general completeness result in refinement (submitted).","key":"39_CR13"},{"unstructured":"Lambek, J., Scott, P.J.: Introduction to Higher-Order Categorical Logic, Cambridge Studies in Advanced Mathematics 7. CUP (1986).","key":"39_CR14"},{"doi-asserted-by":"crossref","unstructured":"Ma, Q., Reynolds, J.C.: Types, abstraction and parametric polymorphism 2. Math. Found. of Prog. Lang. Sem. Lecture Notes in Computer Science. Springer (1991).","key":"39_CR15","DOI":"10.1007\/3-540-55511-0_1"},{"unstructured":"Mitchell, J.: Foundations for programming languages. Foundations of Computing Series. MIT Press (1996).","key":"39_CR16"},{"unstructured":"Moggi, E.: Computational Lambda-calculus and Monads. Proc LICS 89. IEEE Press (1989) 14\u201323.","key":"39_CR17"},{"key":"39_CR18","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1007\/BF01210999","volume":"7","author":"D.A. Naumann","year":"1995","unstructured":"Naumann, D.A.: Data refinement, call by value, and higher order programs. Formal Aspects of Computing 7 (1995) 752\u2013762.","journal-title":"Formal Aspects of Computing"},{"unstructured":"Power, A.J.: Premonoidal categories as categories with algebraic structure. Theoretical Computer Science (to appear).","key":"39_CR19"},{"unstructured":"Plotkin, G.D., Power, A.J., Sannella, D.T.: A generalised notion of logical relations. (submitted).","key":"39_CR20"},{"key":"39_CR21","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1017\/S0960129597002375","volume":"7","author":"A.J. Power","year":"1997","unstructured":"Power, A.J., Robinson, E.P. Premonoidal categories and notions of computation. Math. Structures in Computer Science 7 (1997) 453\u2013468.","journal-title":"Math. Structures in Computer Science"},{"key":"39_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/BFb0014560","volume-title":"Proc TACS 97","author":"A.J. Power","year":"1997","unstructured":"Power, A.J., Thielecke, H.: Environments, Continuation Semantics and Indexed Categories. Proc TACS 97. LNCS 1281 Abadi and Ito (eds) (1997) 391\u2013414"},{"unstructured":"Tennent, R.D.: Correctness of data representations in ALGOL-like languages. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, A.W. Roscoe (ed.) Prentice-Hall (1994) 405\u2013417.","key":"39_CR23"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48168-0_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T00:10:08Z","timestamp":1586131808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48168-0_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665366","9783540481683"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-48168-0_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"13 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}