{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T00:59:03Z","timestamp":1648947543743},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2007,10,13]],"date-time":"2007-10-13T00:00:00Z","timestamp":1192233600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2008,12]]},"DOI":"10.1007\/s00224-007-9062-1","type":"journal-article","created":{"date-parts":[[2007,10,12]],"date-time":"2007-10-12T15:35:29Z","timestamp":1192203329000},"page":"298-321","source":"Crossref","is-referenced-by-count":0,"title":["A Provably Correct Translation of the \u03bb-Calculus into a Mathematical Model of C++"],"prefix":"10.1007","volume":"43","author":[{"given":"Rose H.","family":"Abdul\u00a0Rauf","sequence":"first","affiliation":[]},{"given":"Ulrich","family":"Berger","sequence":"additional","affiliation":[]},{"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,10,13]]},"reference":[{"key":"9062_CR1","volume-title":"Structure and Interpretation of Computer Programs","author":"H. Abelson","year":"1985","unstructured":"Abelson, H., Sussman, G.J., Sussman, J.: Structure and Interpretation of Computer Programs. MIT Press, Cambridge (1985)"},{"key":"9062_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-45793-3_37","volume-title":"Proceedings of the 16th International Workshop on Computer Science Logic (CSL\u201902)","author":"J. Goubault-Larrecq","year":"2002","unstructured":"Goubault-Larrecq, J., Lasota, S., Nowak, D.: Logical relations for monadic types. In: Bradfield, J.C. (ed.) Proceedings of the 16th International Workshop on Computer Science Logic (CSL\u201902), Edinburgh, Scotland, UK, September 2002. Lecture Notes in Computer Science, vol. 2471, pp. 553\u2013568. Springer, Berlin (2002)"},{"key":"9062_CR3","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. In: Meissner L. (ed.) Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages & Applications (OOPSLA\u201999). ACM SIGPLAN Not. 34(10), 132\u2013146 (1999)","DOI":"10.1145\/320385.320395"},{"key":"9062_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/BFb0037110","volume-title":"Typed Lambda Calculi and Applications","author":"A. Jung","year":"1993","unstructured":"Jung, A., Tiuryn, J.: A new characterization of lambda definability. In: Bezem, M., Groote, J.F. (eds.) Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, vol. 664, pp. 245\u2013257. Springer, Berlin (1993)"},{"key":"9062_CR5","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1145\/289423.289464","volume-title":"ICFP\u00a0\u201998: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming","author":"O. Kiselyov","year":"1998","unstructured":"Kiselyov, O.: Functional style in C++: Closures, late binding, and lambda abstractions. In: ICFP\u00a0\u201998: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, pp.\u00a0337\u2013440. ACM, New York (1998)"},{"key":"9062_CR6","unstructured":"L\u00e4ufer, K.: A framework for higher-order functions in C++. In: COOTS (1995)"},{"key":"9062_CR7","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1145\/351240.351251","volume-title":"ICFP\u201900: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming","author":"B. McNamara","year":"2000","unstructured":"McNamara, B., Smaragdakis, Y.: Functional programming in C++. In: ICFP\u201900: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pp. 118\u2013129. ACM, New York (2000)"},{"issue":"1","key":"9062_CR8","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"9062_CR9","series-title":"Handbook of Logic Comput. Sci.","first-page":"269","volume-title":"Semantic Modelling","author":"L. Ong","year":"1995","unstructured":"Ong, L.: Correspondence between operational and denotational semantics: the full abstraction problem for PCF. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Semantic Modelling. Handbook of Logic Comput. Sci., vol.\u00a04, pp. 269\u2013356. Clarendon, Oxford (1995)"},{"key":"9062_CR10","series-title":"Workshops in Computing","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-1-4471-3182-3_11","volume-title":"IVth Higher Order Workshop, Banff 1990","author":"A.M. Pitts","year":"1991","unstructured":"Pitts, A.M.: Evaluation logic. In: Birtwistle, G. (ed.) IVth Higher Order Workshop, Banff 1990. Workshops in Computing, pp. 162\u2013189. Springer, Berlin (1991)"},{"key":"9062_CR11","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G.D. Plotkin","year":"1977","unstructured":"Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5, 223\u2013255 (1977)","journal-title":"Theor. Comput. Sci."},{"key":"9062_CR12","first-page":"363","volume-title":"To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalisms","author":"G.D. Plotkin","year":"1980","unstructured":"Plotkin, G.D.: Lambda definability in the full type hierarchy. In: Hindley, R., Seldin, J. (eds.) To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalisms, pp. 363\u2013373. Academic Press, New York (1980)"},{"key":"9062_CR13","first-page":"513","volume-title":"IFIP\u201983","author":"J.C. Reynolds","year":"1983","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP\u201983, pp. 513\u2013523. North-Holland, Amsterdam (1983)"},{"key":"9062_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine\u2014Definition, Verification, Validation","author":"R. St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine\u2014Definition, Verification, Validation. Springer, Berlin (2001)"},{"key":"9062_CR15","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"Statman, R.: Logical relations and the typed lambda-calculus. Inf. Control 65, 85\u201397 (1985)","journal-title":"Inf. Control"},{"key":"9062_CR16","unstructured":"Striegnitz, J.: FACT!\u2014the functional side of C++. http:\/\/www.fz-juelich.de\/zam\/FACT (2003)"},{"key":"9062_CR17","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretation of functionals of finite type. J. Symb. Log. 32, 198\u2013212 (1967)","journal-title":"J. Symb. Log."},{"key":"9062_CR18","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9062-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-007-9062-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9062-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,27]],"date-time":"2020-04-27T05:52:12Z","timestamp":1587966732000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-007-9062-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,13]]},"references-count":18,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["9062"],"URL":"https:\/\/doi.org\/10.1007\/s00224-007-9062-1","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10,13]]}}}