{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T07:08:18Z","timestamp":1750489698097},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672579"},{"type":"electronic","value":"9783540464327"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46432-8_11","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:22:02Z","timestamp":1184588522000},"page":"161-176","source":"Crossref","is-referenced-by-count":10,"title":["Constructive Data Refinement in Typed Lambda Calculus"],"prefix":"10.1007","author":[{"given":"Furio","family":"Honsell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Longley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Donald","family":"Sannella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Tarlecki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,5,19]]},"reference":[{"unstructured":"S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. To appear in Information and Computation (1996).","key":"11_CR1"},{"key":"11_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/10703163_23","volume-title":"Proc. Computer Science Logic, CSL\u201998","author":"T. Altenkirch","year":"1998","unstructured":"T. Altenkirch. Logical relations and inductive\/coinductive types. Proc. Computer Science Logic, CSL\u201998. Springer LNCS 1584, 343\u2013354 (1998)."},{"doi-asserted-by":"crossref","unstructured":"M. Beeson. Foundations of Constructive Mathematics. Springer (1985).","key":"11_CR3","DOI":"10.1007\/978-3-642-68952-9"},{"issue":"5","key":"11_CR4","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1109\/TSE.1984.5010277","volume":"SE-10","author":"J. Goguen","year":"1984","unstructured":"J. Goguen. Parameterized programming. IEEE Trans. on Software Engineering SE-10(5):528\u2013543 (1984).","journal-title":"IEEE Trans. on Software Engineering"},{"key":"11_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/3-540-48168-0_37","volume-title":"Proc. Computer Science Logic, CSL\u201999","author":"J. Hannay","year":"1999","unstructured":"J. Hannay. Specification refinement with System F. Proc. Computer Science Logic, CSL\u201999, Madrid. Springer LNCS 1683, 530\u2013545 (1999)."},{"key":"11_CR6","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"C.A.R. Hoare. Correctness of data representations. Acta Informatica 1:271\u2013281 (1972).","journal-title":"Acta Informatica"},{"key":"11_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/3-540-48168-0_38","volume-title":"Proc. Computer Science Logic, CSL\u201999","author":"F. Honsell","year":"1999","unstructured":"F. Honsell and D. Sannella. Pre-logical relations. Proc. Computer Science Logic, CSL\u201999, Madrid. Springer LNCS 1683, 546\u2013561 (1999)."},{"key":"11_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BFb0014552","volume-title":"Proc. TACS\u201997","author":"Y. Kinoshita","year":"1997","unstructured":"Y. Kinoshita, P. O\u2019Hearn, J. Power, M. Takeyama and R. Tennent. An axiomatic approach to binary logical relations with applications to data refinement. Proc. TACS\u201997. Springer LNCS 1281, 191\u2013212 (1997)."},{"unstructured":"R. Milner. An algebraic definition of simulation between programs. Proc. 2nd Intl. Joint Conf. on Artificial Intelligence. British Computer Society, 481\u2013489 (1971).","key":"11_CR9"},{"unstructured":"J. Mitchell. Foundations for Programming Languages. MIT Press (1996).","key":"11_CR10"},{"key":"11_CR11","series-title":"Lect Notes Comput Sci","first-page":"225","volume-title":"Proc. Logics of Programs","author":"J. Mitchell","year":"1997","unstructured":"J. Mitchell and A. Meyer. Second-order logical relations. Proc. Logics of Programs, Brooklyn. Springer LNCS 193, 225\u2013236 (1997)."},{"unstructured":"D. Normann. The continuous functionals of finite types over the reals. Technical Report 19, Dept. of Mathematics, University of Oslo (1998).","key":"11_CR12"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G. Plotkin","year":"1977","unstructured":"G. Plotkin. LCF considered as a programming language. Theoretical Computer Science 5:223\u2013255 (1977).","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"G. Plotkin, J. Power, D. Sannella and R. Tennent. Lax logical relations. Submitted for publication (2000).","key":"11_CR14","DOI":"10.1007\/3-540-45022-X_9"},{"unstructured":"D. Plume. A calculator for exact real number computation. B.Sc. project report, Univ. of Edinburgh; available from ftp:\/\/ftp.tardis.ed.ac.uk\/users\/dbp\/report.ps.gz (1998).","key":"11_CR15"},{"unstructured":"J. Reynolds. The Craft of Programming. Prentice Hall (1981).","key":"11_CR16"},{"unstructured":"J. Reynolds. Types, abstraction and parametric polymorphism. Proc. 9th IFIP World Computer Congress, Paris. North Holland, 513\u2013523 (1983).","key":"11_CR17"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1007\/BF01191893","volume":"29","author":"D. Sannella","year":"1992","unstructured":"D. Sannella, S. Soko lowski and A. Tarlecki. Toward formal development of programs from algebraic specifications: parameterisation revisited. Acta Informatica 29:689\u2013736 (1992).","journal-title":"Acta Informatica"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF02737104","volume":"25","author":"D. Sannella","year":"1988","unstructured":"D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25:233\u2013281 (1988).","journal-title":"Acta Informatica"},{"key":"11_CR20","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/BF01211084","volume":"9","author":"D. Sannella","year":"1997","unstructured":"D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9:229\u2013269 (1997).","journal-title":"Formal Aspects of Computing"},{"unstructured":"O. Schoett. Data Abstraction and the Correctness of Modular Programming. Ph.D. thesis, report CST-42-87, Dept. of Computer Science, Univ. of Edinburgh (1987).","key":"11_CR21"},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0167-6423(90)90057-K","volume":"14","author":"O. Schoett","year":"1990","unstructured":"O. Schoett. Behavioural correctness of data representations. Science of Computer Programming 14:43\u201357 (1990).","journal-title":"Science of Computer Programming"},{"key":"11_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/BFb0055795","volume-title":"Proc. 23rd Intl. Symp. on Mathematical Foundations of Computer Science","author":"A.K. Simpson","year":"1998","unstructured":"A.K. Simpson. Lazy functional algorithms for exact real functionals. Proc. 23rd Intl. Symp. on Mathematical Foundations of Computer Science, Brno. Springer LNCS 1450, 456\u2013464 (1998)."},{"unstructured":"R. Tennent. Correctness of data representations in Algol-like languages. In: A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall (1994).","key":"11_CR24"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46432-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:32:06Z","timestamp":1556667126000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46432-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672579","9783540464327"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-46432-8_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}