{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:49:43Z","timestamp":1725493783999},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540140313"},{"type":"electronic","value":"9783540391852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-39185-1_17","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T20:13:43Z","timestamp":1193429623000},"page":"299-315","source":"Crossref","is-referenced-by-count":1,"title":["Monad Translating Inductive and Coinductive Types"],"prefix":"10.1007","author":[{"given":"Tarmo","family":"Uustalu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"17_CR1","volume-title":"Electr. Notes in Theor. Comput. Sci.","author":"A. Abel","year":"2001","unstructured":"Abel, A.: A third-order representation of the \u03bb\u03bc-calculus. In: Ambler, S. J., Crole, R. L., Momigliano, A. (eds.): Proc. of Wksh. on Mechanised Reasoning about Languages with Variable Binding, MERLIN 2001 (Siena, June 2001). Electr. Notes in Theor. Comput. Sci., Vol. 58(1). Elsevier, Amsterdam (2001)"},{"issue":"2","key":"17_CR2","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1023\/A:1010000206149","volume":"12","author":"G. Barthe","year":"1999","unstructured":"Barthe, G., Hatcliff, J., S\u00f8rensen, M. H. B.: CPS translations and applications: The cube and beyond. Higher-Order and Symbolic Comput. 12(2) (1999) 125\u2013170","journal-title":"Higher-Order and Symbolic Comput."},{"key":"17_CR3","volume-title":"Electr. Notes in Theor. Comput. Sci.","author":"G. Barthe","year":"1998","unstructured":"Barthe, G., Hatcliff, J., Thiemann, P.: Monadic type systems: Pure type systems for impure settings (preliminary report). In: Gordon, A., Pitts, A., Talcott, C. (eds.): Proc. of 2nd Wksh. on Higher-Order Operational Techniques in Semantics, HOOTS\u201997 (Stanford Univ., CA, Dec. 1997). Electr. Notes in Theor. Comput. Sci., Vol. 10. Elsevier, Amsterdam (1998)"},{"key":"17_CR4","first-page":"131","volume-title":"SIGPLAN Notices","author":"G. Barthe","year":"2002","unstructured":"Barthe, G., Uustalu, T.: CPS translating inductive and coinductive types (extended abstract). In: Proc. of 2002 ACM SIGPLAN Wksh. on Partial Evaluation and Semantics-Based Program Manipulation, PEPM\u201902 (Portland, OR, Jan. 2002). SIGPLAN Notices 37(3). ACM Press, New York (2002) 131\u2013142"},{"issue":"2","key":"17_CR5","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1017\/S0956796898002998","volume":"8","author":"P. N. Benton","year":"1998","unstructured":"Benton, P. N., Bierman, G. M., de Paiva, V. C. V.: Computational types from a logical perspective. J. of Funct. Prog. 8(2) (1998) 177\u2013193","journal-title":"J. of Funct. Prog."},{"key":"17_CR6","unstructured":"Cockett, R., Fukushima, T.: About Charity. Yellow Series Report 92\/480\/18, Dept. of Computer Science, Univ. of Calgary (1992)"},{"issue":"4","key":"17_CR7","doi-asserted-by":"publisher","first-page":"249","DOI":"10.2307\/2266613","volume":"17","author":"H. B. Curry","year":"1952","unstructured":"Curry, H. B.: The elimination theorem when modality is present. J. of Symb. Logic 17(4) (1952) 249\u2013265","journal-title":"J. of Symb. Logic"},{"issue":"1","key":"17_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M. Fairtlough","year":"1997","unstructured":"Fairtlough, M., Mendler, M.: Propositional lax logic. Inform. and Comput. 137(1) (1997) 1\u201333","journal-title":"Inform. and Comput."},{"key":"17_CR9","unstructured":"Geuvers, H.: Inductive and coinductive types with iteration and recursion. In: Nordstr\u00f6m, B., Pettersson, K., Plotkin, G. (eds.): Proc. of Wksh. on Types for Proofs and Programs (B\u00e5astad, June 1992). Dept. of Computing Science, Chalmers Univ. of Technology and G\u00f6teborg Univ. (1992) 193\u2013217"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/174675.178053","volume-title":"Conf. Record of 21st Ann. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL\u201994 (Portland, OR, Jan. 1994)","author":"J. Hatcliff","year":"1994","unstructured":"Hatcliff, J., Danvy, O.: A generic account of continuation passing styles. In: Conf. Record of 21st Ann. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL\u201994 (Portland, OR, Jan. 1994). ACM Press, New York (1994) 458\u2013471"},{"key":"17_CR11","series-title":"APIC Studies in Data Processing","first-page":"279","volume-title":"Logic and Computer Science","author":"D. Leivant","year":"1990","unstructured":"Leivant, D.: Contracting proofs to programs. In: Odifreddi, P. (ed.): Logic and Computer Science. APIC Studies in Data Processing, Vol. 31. Academic Press, London (1990) 279\u2013327"},{"key":"17_CR12","first-page":"30","volume-title":"Proc. of 2nd Ann. IEEE Symp. on Logic in Computer Science, LICS\u201987 (Ithaca, NY, June 1987)","author":"N. P. Mendler","year":"1987","unstructured":"Mendler, N. P.: Recursive types and type constraints in second-order lambda-calculus. In: Proc. of 2nd Ann. IEEE Symp. on Logic in Computer Science, LICS\u201987 (Ithaca, NY, June 1987). IEEE CS Press, Washington, DC (1987) 30\u201336"},{"issue":"1\u20132","key":"17_CR13","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","volume":"51","author":"N. P. Mendler","year":"1991","unstructured":"Mendler, N. P.: Inductive types and type constraints in the second-order lambda-calculus. Ann. of Pure and Appl. Logic, 51(1\u20132) (1991) 159\u2013172","journal-title":"Ann. of Pure and Appl. Logic"},{"issue":"1","key":"17_CR14","doi-asserted-by":"publisher","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. Inform. and Comput. 93(1) (1991) 55\u201392","journal-title":"Inform. and Comput."},{"key":"17_CR15","series-title":"Lect. Notes in Artif. Intell.","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Proc. of Int. Conf. on Logic Programming and Automated Reasoning, LPAR\u201992 (St Petersburg, July 1992)","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: \u03bb\u03bc-calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.): Proc. of Int. Conf. on Logic Programming and Automated Reasoning, LPAR\u201992 (St Petersburg, July 1992). Lect. Notes in Artif. Intell., Vol. 624. Springer-Verlag, Berlin (1992) 190\u2013201"},{"issue":"2","key":"17_CR16","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. D. Plotkin","year":"1975","unstructured":"Plotkin, G. D:: Call-by-name, call-by-value and the \u03bb-calculus. Theor. Comput. Sci. 1(2) (1975) 125\u2013159","journal-title":"Theor. Comput. Sci."},{"key":"17_CR17","first-page":"102","volume-title":"SIGPLAN Notices","author":"Z. Sp\u0142awski","year":"1999","unstructured":"Sp\u0142awski, Z., Urzyczyn, P.: Type fixpoints: Iteration vs. recursion. In: Proc. of 4th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP\u201999 (Paris, Sept. 1999). SIGPLAN Notices 34(9). ACM Press, New York (1999) 102\u2013113"},{"issue":"4","key":"17_CR18","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1017\/S0960129500001560","volume":"2","author":"P. Wadler","year":"1992","unstructured":"Wadler, P.: Comprehending monads. Math. Struct. in Comp. Sci. 2(4) (1992) 461\u2013493","journal-title":"Math. Struct. in Comp. Sci."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-39185-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T16:10:03Z","timestamp":1551024603000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-39185-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540140313","9783540391852"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-39185-1_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}