{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:50:17Z","timestamp":1760043017710,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2004,9,22]],"date-time":"2004-09-22T00:00:00Z","timestamp":1095811200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2004,9,22]]},"DOI":"10.1145\/1017472.1017477","type":"proceedings-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:39:48Z","timestamp":1097170788000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Functional pearl"],"prefix":"10.1145","author":[{"given":"Conor","family":"McBride","sequence":"first","affiliation":[{"name":"University of Durham, Durham, England"}]},{"given":"James","family":"McKinna","sequence":"additional","affiliation":[{"name":"University of St Andrews, St Andrews, Scotland"}]}],"member":"320","published-online":{"date-parts":[[2004,9,22]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"1999","article-title":"Monadic presentations of lambda-terms using generalized inductive types","author":"Altenkirch T.","year":"1999","unstructured":"T. Altenkirch and B. Reus . Monadic presentations of lambda-terms using generalized inductive types . In Computer Science Logic 1999 , 1999 .]] T. Altenkirch and B. Reus. Monadic presentations of lambda-terms using generalized inductive types. In Computer Science Logic 1999, 1999.]]","journal-title":"Computer Science Logic"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00022-0"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003366"},{"key":"e_1_3_2_1_4_1","unstructured":"T. Coquand. An algorithm for testing conversion in type theory. In Huet and Plotkin {11}.]] T. Coquand. An algorithm for testing conversion in type theory. In Huet and Plotkin {11}.]]"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_6_1","volume-title":"Duckworth","author":"de Saussure F.","year":"1983","unstructured":"F. de Saussure . Course in General Linguistics . Duckworth , 1983 . English translation by Roy Harris.]] F. de Saussure. Course in General Linguistics. Duckworth, 1983. English translation by Roy Harris.]]"},{"key":"e_1_3_2_1_7_1","unstructured":"P. Dybjer. Inductive Sets and Families in Martin-L\u00f6f's Type Theory. In Huet and Plotkin {11}.]] P. Dybjer. Inductive Sets and Families in Martin-L\u00f6f's Type Theory. In Huet and Plotkin {11}.]]"},{"key":"e_1_3_2_1_8_1","volume-title":"North-Holland","author":"Gentzen G.","year":"1969","unstructured":"G. Gentzen . The collected papers of Gerhard Gentzen . North-Holland , 1969 . Edited by Manfred Szabo.]] G. Gentzen. The collected papers of Gerhard Gentzen. North-Holland, 1969. Edited by Manfred Szabo.]]"},{"key":"e_1_3_2_1_9_1","volume-title":"The Constructive Engine","author":"Huet G.","year":"1989","unstructured":"G. Huet . The Constructive Engine . In R. Narasimhan, editor, A Perspective in Theoretical Computer Science. World Scientific Publishing , 1989 . Commemorative Volume for Gift Siromoney.]] G. Huet. The Constructive Engine. In R. Narasimhan, editor, A Perspective in Theoretical Computer Science. World Scientific Publishing, 1989. Commemorative Volume for Gift Siromoney.]]"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002864"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/120477"},{"key":"e_1_3_2_1_12_1","first-page":"190","volume-title":"Jouannaud {13}","author":"Johnsson T.","unstructured":"T. Johnsson . Lambda Lifting: Transforming Programs to Recursive Equations . In Jouannaud {13} , pages 190 -- 203 .]] T. Johnsson. Lambda Lifting: Transforming Programs to Recursive Equations. In Jouannaud {13}, pages 190--203.]]"},{"key":"e_1_3_2_1_13_1","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-15975-4","volume-title":"Functional Programming Languages and Computer Architecture","author":"Jouannaud J.-P.","year":"1985","unstructured":"J.-P. Jouannaud , editor. Functional Programming Languages and Computer Architecture , volume 201 of LNCS . Springer-Verlag , 1985 .]] J.-P. Jouannaud, editor. Functional Programming Languages and Computer Architecture, volume 201 of LNCS. Springer-Verlag, 1985.]]"},{"key":"e_1_3_2_1_14_1","volume-title":"Introduction to Metamathematics. van Nostrand Rheinhold","author":"Kleene S.","year":"1952","unstructured":"S. Kleene . Introduction to Metamathematics. van Nostrand Rheinhold , Princeton , 1952 .]] S. Kleene. Introduction to Metamathematics. van Nostrand Rheinhold, Princeton, 1952.]]"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and Reasoning: A Type Theory for Computer Science","author":"Luo Z.","year":"1994","unstructured":"Z. Luo . Computation and Reasoning: A Type Theory for Computer Science . Oxford University Press , 1994 .]] Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994.]]"},{"key":"e_1_3_2_1_16_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/BFb0097795","volume-title":"Types for Proofs and Programs, '96","author":"McBride C.","year":"1998","unstructured":"C. McBride . Inverting inductively defined relations in LEGO . In E. Gim\u00e9nez and C. Paulin-Mohring, editors, Types for Proofs and Programs, '96 , volume 1512 of LNCS , pages 236 -- 253 . Springer-Verlag , 1998 .]] C. McBride. Inverting inductively defined relations in LEGO. In E. Gim\u00e9nez and C. Paulin-Mohring, editors, Types for Proofs and Programs, '96, volume 1512 of LNCS, pages 236--253. Springer-Verlag, 1998.]]"},{"key":"e_1_3_2_1_17_1","series-title":"LNCS","volume-title":"Types for Proofs and Programs (Proceedings of the International Workshop, TYPES'00)","author":"McBride C.","year":"2002","unstructured":"C. McBride . Elimination with a Motive . In P. Callaghan, Z. Luo, J. McKinna, and R. Pollack, editors, Types for Proofs and Programs (Proceedings of the International Workshop, TYPES'00) , volume 2277 of LNCS . Springer-Verlag , 2002 .]] C. McBride. Elimination with a Motive. In P. Callaghan, Z. Luo, J. McKinna, and R. Pollack, editors, Types for Proofs and Programs (Proceedings of the International Workshop, TYPES'00), volume 2277 of LNCS. Springer-Verlag, 2002.]]"},{"key":"e_1_3_2_1_18_1","unstructured":"C. McBride. Epigram 2004. http:\/\/www.dur.ac.uk\/CARG\/epigram.]] C. McBride. Epigram 2004. http:\/\/www.dur.ac.uk\/CARG\/epigram.]]"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_20_1","series-title":"LNCS","volume-title":"M. Bezem and J.-F","author":"McKinna J.","year":"1993","unstructured":"J. McKinna and R. Pollack . Pure type systems formalized . In M. Bezem and J.-F . Groote, editors, Int. Conf. Typed Lambda Calculi and Applications TLCA'93, volume 664 of LNCS . Springer-Verlag , 1993 .]] J. McKinna and R. Pollack. Pure type systems formalized. In M. Bezem and J.-F. Groote, editors, Int. Conf. Typed Lambda Calculi and Applications TLCA'93, volume 664 of LNCS. Springer-Verlag, 1993.]]"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"e_1_3_2_1_23_1","volume-title":"Springer-Verlag, 1994. Selected papers from the Int. Workshop TYPES '93","author":"Pollack R.","year":"1993","unstructured":"R. Pollack . Closure under alpha-conversion. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, LNCS 806, pages 313--332 . Springer-Verlag, 1994. Selected papers from the Int. Workshop TYPES '93 , Nijmegen , May 1993 .]] R. Pollack. Closure under alpha-conversion. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, LNCS 806, pages 313--332. Springer-Verlag, 1994. Selected papers from the Int. Workshop TYPES '93, Nijmegen, May 1993.]]"},{"key":"e_1_3_2_1_24_1","volume-title":"Almquist and Wiksell","author":"Prawitz D.","year":"1965","unstructured":"D. Prawitz . Natural Deduction-A proof theoretical study . Almquist and Wiksell , Stockholm , 1965 .]] D. Prawitz. Natural Deduction-A proof theoretical study. Almquist and Wiksell, Stockholm, 1965.]]"},{"key":"e_1_3_2_1_25_1","first-page":"113","volume-title":"Jouannaud {13}","author":"Wadler P.","unstructured":"P. Wadler . How to Replace Failure by a list of Successes . In Jouannaud {13} , pages 113 -- 128 .]] P. Wadler. How to Replace Failure by a list of Successes. In Jouannaud {13}, pages 113--128.]]"}],"event":{"name":"HW04: Haskell Workshop 2004","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Snowbird Utah USA","acronym":"HW04"},"container-title":["Proceedings of the 2004 ACM SIGPLAN workshop on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1017472.1017477","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1017472.1017477","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:24:59Z","timestamp":1750263899000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1017472.1017477"}},"subtitle":["i am not a number--i am a free variable"],"short-title":[],"issued":{"date-parts":[[2004,9,22]]},"references-count":25,"alternative-id":["10.1145\/1017472.1017477","10.1145\/1017472"],"URL":"https:\/\/doi.org\/10.1145\/1017472.1017477","relation":{},"subject":[],"published":{"date-parts":[[2004,9,22]]},"assertion":[{"value":"2004-09-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}