{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:40:43Z","timestamp":1725496843972},"publisher-location":"Berlin, Heidelberg","reference-count":14,"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_38","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T06:30:26Z","timestamp":1196490626000},"page":"546-561","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Pre-logical Relations"],"prefix":"10.1007","author":[{"given":"Furio","family":"Honsell","sequence":"first","affiliation":[]},{"given":"Donald","family":"Sannella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"38_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1093\/logcom\/1.1.5","volume":"1","author":"S. Abramsky","year":"1990","unstructured":"S. Abramsky. Abstract interpretation, logical relations, and Kan extensions. Journal of Logic and Computation 1:5\u201340 (1990).","journal-title":"Journal of Logic and Computation"},{"key":"38_CR2","unstructured":"R. Gandy. Proofs of strong normalization. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 457\u2013477. Academic Press (1980)."},{"key":"38_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/BFb0037110","volume-title":"Proc. TLCA\u201993","author":"A. Jung","year":"1993","unstructured":"A. Jung and J. Tiuryn. A new characterization of lambda definability. Proc. TLCA\u201993. Springer LNCS 664, 245\u2013257 (1993)."},{"key":"38_CR4","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)."},{"key":"38_CR5","doi-asserted-by":"crossref","unstructured":"J. Mitchell. Type Systems for Programming Languages. Chapter 8 of Handbook of Theoretical Computer Science, Vol B. Elsevier (1990).","DOI":"10.1016\/B978-0-444-88074-1.50013-5"},{"key":"38_CR6","unstructured":"J. Mitchell. Foundations for Programming Languages. MIT Press (1996)."},{"key":"38_CR7","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0168-0072(91)90067-V","volume":"51","author":"J. Mitchell","year":"1991","unstructured":"J. Mitchell and E. Moggi. Kripke-style models for typed lambda calculus. Annals of Pure And Applied Logic 51:99\u2013124 (1991).","journal-title":"Annals of Pure And Applied Logic"},{"key":"38_CR8","unstructured":"G. Plotkin. Lambda-definability in the full type hierarchy. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 363\u2013373. Academic Press (1980)."},{"key":"38_CR9","unstructured":"G. Plotkin, J. Power and D. Sannella. A compositional generalisation of logical relations. Draft report, http:\/\/www.dcs.ed.ac.uk\/home\/dts\/pub\/laxlogrel.ps (1998)."},{"key":"38_CR10","unstructured":"E. Robinson. Logical relations and data abstraction. Report 730, Queen Mary and Westfield College (1996)."},{"key":"38_CR11","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF00283329","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":"38_CR12","unstructured":"O. Schoett. Data Abstraction and the Correctness of Modular Programming. Ph.D. thesis CST-42-87, Univ. of Edinburgh (1987)."},{"key":"38_CR13","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"R. Statman. Logical relations and the typed lambda calculus. Information and Control 65:85\u201397 (1985).","journal-title":"Information and Control"},{"key":"38_CR14","unstructured":"R. Tennent. Correctness of data representations in Algol-like languages. In: AClassic al Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall (1994)."}],"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_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T00:10:04Z","timestamp":1586131804000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48168-0_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665366","9783540481683"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-48168-0_38","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"}}]}}