{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T05:10:21Z","timestamp":1736140221281,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540633884"},{"type":"electronic","value":"9783540695301"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"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":[[1997]]},"DOI":"10.1007\/bfb0014552","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:17:33Z","timestamp":1132737453000},"page":"191-212","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["An axiomatic approach to binary logical relations with applications to data refinement"],"prefix":"10.1007","author":[{"given":"Yoshiki","family":"Kinoshita","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter W.","family":"O'Hearnt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. John","family":"Power","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Makoto","family":"Takeyama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert D.","family":"Tennent","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Michael Barr and Charles Wells. Toposes, Triples and Theories, volume 278 of Grundlagen der mathentatischen Wissenschaften. Springer-Verlag, 1985.","DOI":"10.1007\/978-1-4899-0021-0"},{"volume-title":"Programming Methodology, A Collection of Articles by IFIP WG 2.3","year":"1978","key":"8_CR2","unstructured":"D. Gries, editor. Programming Methodology, A Collection of Articles by IFIP WG 2.3. Springer-Verlag, New York, 1978."},{"key":"8_CR3","unstructured":"Claudio A. Hermida. Fibrations, Logical Predicates, and Indeterminates. PhD thesis, The University of Edinburgh, 1993. Published as CST-103-93, also as ECS-LFCS-93-277."},{"key":"8_CR4","unstructured":"C.A.R. Hoare. Data refinement in a categorical setting. Unpublished manuscript, 1987."},{"key":"8_CR5","unstructured":"C.A.R. Hoare and He Jifeng. Data refinement in a categorical setting. Oxford Computing Laboratory Technical Monograph PRG-90, 1990."},{"key":"8_CR6","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/0022-4049(93)90092-8","volume":"89","author":"G.M. Kelly","year":"1993","unstructured":"G.M. Kelly and A.J. Power. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra, 89:163\u2013179, 1993.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"8_CR7","unstructured":"Y. Kinoshita and A.J. Power. Data refinement and algebraic structure. ETL Technical Report TR96-2, Electrotechnical Laboratory, January 1996."},{"issue":"1","key":"8_CR8","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/0022-4049(95)00136-0","volume":"112","author":"Y. Kinoshita","year":"1996","unstructured":"Y. Kinoshita and A.J. Power. Lax naturality through enrichment. Journal of Pure and Applied Algebra, 112(1):53\u201372, 1996.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"8_CR9","unstructured":"Yoshiki Kinoshita, A. John Power, and Makoto Takeyama. Sketches. Submitted, 1996."},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Mathematical Foundations of Programming Semantics","author":"Q. Ma","year":"1992","unstructured":"QingMing Ma and J. C. Reynolds. Types, abstraction, and parametric polymorphism, part 2. In S. Brookes et al., editors, Mathematical Foundations of Programming Semantics, Proceedings of the 7th International Conference, volume 598 of Lecture Notes in Computer Science, pages 1\u201340. Springer-Verlag, Berlin, 1992, Pittsburgh, PA, March 1991."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"J. C. Mitchell. Representation independence and data abstraction. pages 263\u2013276.","DOI":"10.1145\/512644.512669"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","first-page":"352","volume-title":"Computer Science Logic: 6th Workshop, CSL '92: Selected Papers","author":"J.C. Mitchell","year":"1992","unstructured":"J.C. Mitchell and A. Scedrov. Notes on sconing and relators. In E. Boerger et al., editors, Computer Science Logic: 6th Workshop, CSL '92: Selected Papers, volume 702 of Lecture Notes in Computer Science, pages 352\u2013378, San Miniato, Italy, 1992. Springer-Verlag, Berlin."},{"issue":"3","key":"8_CR13","doi-asserted-by":"crossref","first-page":"658","DOI":"10.1145\/210346.210425","volume":"42","author":"P. W. O'Hearn","year":"1995","unstructured":"P. W. O'Hearn and R. D. Tennent. Parametricity and local variables. J. ACM, 42(3):658\u2013709, May 1995. Also in [14].","journal-title":"J. ACM"},{"volume-title":"Algol-like Languages","year":"1997","key":"8_CR14","unstructured":"P.W. O'Hearn and R.D. Tennent, editors. Algol-like Languages, volume 2. Birkhauser, Boston, 1997."},{"key":"8_CR15","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1006\/inco.1996.0052","volume":"127","author":"A. M. Pitts","year":"1996","unstructured":"A. M. Pitts. Relational properties of domains. Information and Computation, 127:66\u201390, 1996.","journal-title":"Information and Computation"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BFb0037118","volume-title":"Typed Lambda Calculi and Applications","author":"G. Plotkin","year":"1993","unstructured":"G. Plotkin and M. Abadi. A logic for parametric polymorphism. In M. Bezen and J. F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 361\u2013375, Utrecht, The Netherlands, March 1993. Springer-Verlag, Berlin."},{"key":"8_CR17","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G. D. Plotkin","year":"1977","unstructured":"G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223\u2013255, 1977.","journal-title":"Theoretical Computer Science"},{"key":"8_CR18","unstructured":"A. J. Power. Premonoidal categories as categories with algebraic structure. Submitted."},{"key":"8_CR19","first-page":"157","volume-title":"New Advances in Algorithmic Languages 1975","author":"J. C. Reynolds","year":"1975","unstructured":"J. C. Reynolds. User-defined types and procedural data structures as complementary approaches to data abstraction. In S. A. Schuman, editor, New Advances in Algorithmic Languages 1975, pages 157\u2013168. Inst. de Reserche d'Informatique et d'Automatique, Rocquencourt, France, 1975. Reprinted in [2], pages 309\u2013317."},{"key":"8_CR20","first-page":"513","volume-title":"Information. Processing 83","author":"J. C. Reynolds","year":"1983","unstructured":"J. C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information. Processing 83, pages 513\u2013523. North Holland, Amsterdam, 1983."},{"key":"8_CR21","unstructured":"E. P. Robinson. Logical relations and data abstraction. Extended abstract."},{"key":"8_CR22","volume-title":"Proceedings, 9th Annual IEEE Symposium on Logic in Computer Science","author":"E. P. Robinson","year":"1994","unstructured":"E. P. Robinson and G. Rosolim. Reflexive graphs and parametric polymorphism. In Proceedings, 9th Annual IEEE Symposium on Logic in Computer Science, Paris, 1994. IEEE Computer Society Press, Los Alamitos, California."},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"D. S. Scott. A type-theoretical alternative to CUCH, ISWIM, OWHY. Privately circulated memo, Oxford University, October 1969. Published in Theoretical Computer Science, 121(1\/2):411\u2013440, 1993.","DOI":"10.1016\/0304-3975(93)90095-B"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"H. Thielecke. Continuation passing style and self adjointness. Continuations Workshop, Paris, January, 1997.","DOI":"10.1016\/S1571-0661(05)80149-5"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014552","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T21:50:21Z","timestamp":1736113821000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014552"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633884","9783540695301"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/bfb0014552","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}