{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:09:50Z","timestamp":1763467790814},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657637"},{"type":"electronic","value":"9783540489597"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48959-2_12","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T12:52:16Z","timestamp":1178196736000},"page":"147-161","source":"Crossref","is-referenced-by-count":10,"title":["Lambda Definability with Sums via Grothendieck Logical Relations"],"prefix":"10.1007","author":[{"given":"Marcelo","family":"Fiore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alex","family":"Simpson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,27]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/0304-3975(94)00283-O","volume":"146","author":"M. Alimohamed","year":"1995","unstructured":"M. Alimohamed. A characterization of lambda definability in categorical models of implicit polymorphism. Theoretical Computer Science, 146:5\u201323, 1995.","journal-title":"Theoretical Computer Science"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"D. Dougherty and R. Subrahmanyam. Equality between functionals in the presence of coproducts. Submitted to Information and Computation. An earlier version appeared in Proceedings of 10th LICS, pages 282\u2013291, 1995.","DOI":"10.1109\/LICS.1995.523263"},{"key":"12_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/BFb0014052","volume-title":"Typed Lambda Calculi and Applications, Proceedings of TLCA\u2019 95","author":"N. Ghani","year":"1995","unstructured":"N. Ghani. \u03b2\u03b7-equality for coproducts. In Typed Lambda Calculi and Applications, Proceedings of TLCA\u2019 95, pages 171\u2013185. Springer LNCS 902, 1995."},{"key":"12_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/BFb0037109","volume-title":"Typed Lambda Calculi and Applications, Proceedings of TLCA\u2019 93","author":"A. Jung","year":"1993","unstructured":"A. Jung and J. Tiuryn. A new characterisation of lambda definability. In Typed Lambda Calculi and Applications, Proceedings of TLCA\u2019 93, pages 230\u2013244. Springer LNCS 664, 1993."},{"key":"12_CR5","unstructured":"J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Number 7 in Cambridge studies in advanced mathematics. Cambridge University Press, 1986."},{"key":"12_CR6","unstructured":"S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag, 1992."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume II, pages 365\u2013458. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50013-5"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1006\/inco.1995.1103","volume":"120","author":"P.W. O\u2019Hearn","year":"1995","unstructured":"P.W. O\u2019Hearn and J.G. Riecke. Kripke logical relations and PCF. Information and Computation, 120:107\u2013116, 1995.","journal-title":"Information and Computation"},{"key":"12_CR9","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1002\/malq.19970430304","volume":"43","author":"E. Palmgren","year":"1997","unstructured":"E. Palmgren. Constructive sheaf semantics. Mathematical Logic Quarterly, 43:321\u2013325, 1997.","journal-title":"Mathematical Logic Quarterly"},{"key":"12_CR10","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"G.D. Plotkin","year":"1980","unstructured":"G.D. Plotkin. Lambda-definability in the full type hierarchy. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, 1980."},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"J.G. Riecke and A.B. Sandholm. A relational account of call-by-value sequentiality. In Proceedings of 12th Annual Symposium on Logic in Computer Science, pages 258\u2013267, 1997.","DOI":"10.1109\/LICS.1997.614953"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1016\/0022-4049(74)90014-0","volume":"4","author":"G. Wraith","year":"1974","unstructured":"G. Wraith. Artin glueing. Journal of Pure and Applied Algebra, 4:345\u2013348, 1974.","journal-title":"Journal of Pure and Applied Algebra"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48959-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T07:37:53Z","timestamp":1550302673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48959-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657637","9783540489597"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-48959-2_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}