{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:37:42Z","timestamp":1767926262066,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,9,26]],"date-time":"2010-09-26T00:00:00Z","timestamp":1285459200000},"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":[[2010,9,26]]},"DOI":"10.1145\/1863495.1863497","type":"proceedings-article","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T17:41:50Z","timestamp":1285695710000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Outrageous but meaningful coincidences"],"prefix":"10.1145","author":[{"given":"Conor","family":"McBride","sequence":"first","affiliation":[{"name":"University of Strathclyde, Glasgow, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2010,9,26]]},"reference":[{"key":"e_1_3_2_2_1_1","series-title":"IFIP Conference Proceedings","first-page":"1","volume-title":"Generic Programming","author":"Altenkirch T.","year":"2002","unstructured":"}} T. Altenkirch and C. McBride . Generic programming within dependently typed programming . In J. Gibbons and J. Jeuring, editors, Generic Programming , volume 243 of IFIP Conference Proceedings , pages 1 -- 20 . Kluwer , 2002 . }}T. Altenkirch and C. McBride. Generic programming within dependently typed programming. In J. Gibbons and J. Jeuring, editors, Generic Programming, volume 243 of IFIP Conference Proceedings, pages 1--20. Kluwer, 2002."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"crossref","unstructured":"}}\n      T.\n      Altenkirch\n     and \n      B.\n      Reus\n  . \n  Monadic presentations of lambda terms using generalized inductive types\n  . In J. Flum and M. Rodr\u00edguez-Artalejo editors CSL volume \n  1683\n   of \n  LNCS pages \n  453\n  --\n  468\n  . \n  Springer 1999\n  .   }}T. Altenkirch and B. Reus. Monadic presentations of lambda terms using generalized inductive types. In J. Flum and M. Rodr\u00edguez-Artalejo editors CSL volume 1683 of LNCS pages 453--468. Springer 1999.","DOI":"10.1007\/3-540-48168-0_32"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_2_4_1","volume-title":"An exercise in dependent types: A well-typed interpreter.","author":"Augustsson L.","year":"1999","unstructured":"}} L. Augustsson and M. Carlsson . An exercise in dependent types: A well-typed interpreter. Available at http:\/\/www.cs.chalmers.se\/~augustss\/cayenne\/interp.ps!, 1999 . }}L. Augustsson and M. Carlsson. An exercise in dependent types: A well-typed interpreter. Available at http:\/\/www.cs.chalmers.se\/~augustss\/cayenne\/interp.ps!, 1999."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017485"},{"key":"e_1_3_2_2_6_1","volume-title":"INRIA","author":"Barras B.","year":"1996","unstructured":"}} B. Barras . Coq en coq. Rapport de Recherche 3026 , INRIA , Oct. 1996 . }}B. Barras. Coq en coq. Rapport de Recherche 3026, INRIA, Oct. 1996."},{"key":"e_1_3_2_2_7_1","volume-title":"Universit\u00e9 Paris","author":"Barras B.","year":"1999","unstructured":"}} B. Barras . Auto-validation d'un syst\u00e8me de preuves avec familles inductives. Th\u00e8se de doctorat , Universit\u00e9 Paris 7, Nov. 1999 . }}B. Barras. Auto-validation d'un syst\u00e8me de preuves avec familles inductives. Th\u00e8se de doctorat, Universit\u00e9 Paris 7, Nov. 1999."},{"key":"e_1_3_2_2_8_1","unstructured":"}}B. Barras and B. Werner. Coq in coq. http:\/\/pauillac.inria.fr\/~barras\/coqincoq.ps.gz 1997.  }}B. Barras and B. Werner. Coq in coq. http:\/\/pauillac.inria.fr\/~barras\/coqincoq.ps.gz 1997."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173724"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863587"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944730"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289459"},{"key":"e_1_3_2_2_18_1","volume-title":"Combinatory Logic","author":"Curry H. B.","year":"1958","unstructured":"}} H. B. Curry and R. Feys . Combinatory Logic Volume I . Studies in Logic. North-Holland , 1958 . }}H. B. Curry and R. Feys. Combinatory Logic Volume I. Studies in Logic. North-Holland, 1958."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"crossref","unstructured":"}}\n      N. A.\n      Danielsson\n    .\n  A formalisation of a dependently typed language as an inductive-recursive family\n  . In T. Altenkirch and C. McBride editors TYPES volume \n  4502\n   of \n  LNCS pages \n  93\n  --\n  109\n  . \n  Springer 2006\n  .   }}N. A. Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In T. Altenkirch and C. McBride editors TYPES volume 4502 of LNCS pages 93--109. Springer 2006.","DOI":"10.1007\/978-3-540-74464-1_7"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90066-B"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/120477.120487"},{"key":"e_1_3_2_2_24_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-45504-3_7","volume-title":"Proof Theory in Computer Science","author":"Dybjer P.","year":"2001","unstructured":"}} P. Dybjer and A. Setzer . Indexed induction-recursion . In R. Kahle, P. Schroeder-Heister, and R. F. St\u00e4rk, editors, Proof Theory in Computer Science , volume 2183 of LNCS , pages 93 -- 113 . Springer , 2001 . }}P. Dybjer and A. Setzer. Indexed induction-recursion. In R. Kahle, P. Schroeder-Heister, and R. F. St\u00e4rk, editors, Proof Theory in Computer Science, volume 2183 of LNCS, pages 93--113. Springer, 2001."},{"key":"e_1_3_2_2_25_1","series-title":"LNCS","first-page":"129","volume-title":"J.-Y","author":"Dybjer P.","year":"1999","unstructured":"}} P. Dybjer and A. Setzer . A finite axiomatization of inductive-recursive definitions . In J.-Y . Girard, editor, TLCA 1999 , volume 1581 of LNCS , pages 129 -- 146 . Springer , 1999. }}P. Dybjer and A. Setzer. A finite axiomatization of inductive-recursive definitions. In J.-Y. Girard, editor, TLCA 1999, volume 1581 of LNCS, pages 129--146. Springer, 1999."},{"key":"e_1_3_2_2_26_1","volume-title":"CSL 2010","author":"Forsberg F.","year":"2010","unstructured":"}} F. Forsberg and A. Setzer . Inductive-inductive definitions . In CSL 2010 . Springer , 2010 . }}F. Forsberg and A. Setzer. Inductive-inductive definitions. In CSL 2010. Springer, 2010."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_2_28_1","volume-title":"Electronic Proceedings of the First Annual BRA Workshop on Logical Frameworks","author":"Huet G.","year":"1990","unstructured":"}} G. Huet and G. Plotkin , editors . Electronic Proceedings of the First Annual BRA Workshop on Logical Frameworks ( Antibes, France) , 1990 . }}G. Huet and G. Plotkin, editors. Electronic Proceedings of the First Annual BRA Workshop on Logical Frameworks (Antibes, France), 1990."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"e_1_3_2_2_30_1","volume-title":"Intuitionistic Type Theory. Bibliopolis\u2022Napoli","author":"Martin-L\u00f6f P.","year":"1984","unstructured":"}} P. Martin-L\u00f6f . Intuitionistic Type Theory. Bibliopolis\u2022Napoli , 1984 . }}P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis\u2022Napoli, 1984."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"crossref","unstructured":"}}\n      J.\n      McKinna\n     and \n      R.\n      Pollack\n  . \n  Pure type systems formalized\n  . In M. Bezem and J. F. Groote editors TLCA volume \n  664\n   of \n  LNCS pages \n  289\n  --\n  305\n  . \n  Springer 1993\n  .   }}J. McKinna and R. Pollack. Pure type systems formalized. In M. Bezem and J. F. Groote editors TLCA volume 664 of LNCS pages 289--305. Springer 1993.","DOI":"10.1007\/BFb0037113"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"e_1_3_2_2_36_1","series-title":"LNCS","first-page":"230","volume-title":"Advanced Functional Programming","author":"Norell U.","year":"2008","unstructured":"}} U. Norell . Dependently typed programming in agda . In P. W. M. Koopman, R. Plasmeijer, and S. D. Swierstra, editors, Advanced Functional Programming , volume 5832 of LNCS , pages 230 -- 266 . Springer , 2008 . }}U. Norell. Dependently typed programming in agda. In P. W. M. Koopman, R. Plasmeijer, and S. D. Swierstra, editors, Advanced Functional Programming, volume 5832 of LNCS, pages 230--266. Springer, 2008."},{"key":"e_1_3_2_2_38_1","volume-title":"Proceedings of the meeting Twenty-five years of constructive type theory. OUP","author":"Palmgren E.","year":"1998","unstructured":"}} E. Palmgren . On universes in type theory . In Proceedings of the meeting Twenty-five years of constructive type theory. OUP , 1998 . }}E. Palmgren. On universes in type theory. In Proceedings of the meeting Twenty-five years of constructive type theory. OUP, 1998."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581499"},{"key":"e_1_3_2_2_40_1","volume-title":"ENS Lyon","author":"Paulin-Mohring C.","year":"1996","unstructured":"}} C. Paulin-Mohring . D\u00e9finitions inductives en th\u00e9orie des types d'ordre sup\u00e9rieur. th\u00e8se d'habilitation , ENS Lyon , 1996 . }}C. Paulin-Mohring. D\u00e9finitions inductives en th\u00e9orie des types d'ordre sup\u00e9rieur. th\u00e8se d'habilitation, ENS Lyon, 1996."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268967"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200018"},{"key":"e_1_3_2_2_44_1","volume-title":"Implicit syntax. URL ftp:\/\/ftp.dcs.ed.ac.uk\/pub\/lego\/ImplicitSyntax.ps.Z. An earlier version appeared in {Huet and Plotkin 1990}","author":"Pollack R.","year":"1992","unstructured":"}} R. Pollack . Implicit syntax. URL ftp:\/\/ftp.dcs.ed.ac.uk\/pub\/lego\/ImplicitSyntax.ps.Z. An earlier version appeared in {Huet and Plotkin 1990} , 1992 . }}R. Pollack. Implicit syntax. URL ftp:\/\/ftp.dcs.ed.ac.uk\/pub\/lego\/ImplicitSyntax.ps.Z. An earlier version appeared in {Huet and Plotkin 1990}, 1992."},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596614.1596616"}],"event":{"name":"ICFP '10: ACM SIGPLAN International Conference on Functional Programming","location":"Baltimore Maryland USA","acronym":"ICFP '10","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 6th ACM SIGPLAN workshop on Generic programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1863495.1863497","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1863495.1863497","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:39:52Z","timestamp":1750246792000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1863495.1863497"}},"subtitle":["dependent type-safe syntax and evaluation"],"short-title":[],"issued":{"date-parts":[[2010,9,26]]},"references-count":41,"alternative-id":["10.1145\/1863495.1863497","10.1145\/1863495"],"URL":"https:\/\/doi.org\/10.1145\/1863495.1863497","relation":{},"subject":[],"published":{"date-parts":[[2010,9,26]]},"assertion":[{"value":"2010-09-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}