{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:54Z","timestamp":1772164014323,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,9,27]],"date-time":"2010-09-27T00:00:00Z","timestamp":1285545600000},"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,27]]},"DOI":"10.1145\/1863543.1863547","type":"proceedings-article","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T13:41:50Z","timestamp":1285681310000},"page":"3-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["The gentle art of levitation"],"prefix":"10.1145","author":[{"given":"James","family":"Chapman","sequence":"first","affiliation":[{"name":"Tallinn University of Technology, Tallinn, Estonia"}]},{"given":"Pierre-\u00c9variste","family":"Dagand","sequence":"additional","affiliation":[{"name":"University of Strathclyde, Glasgow, United Kingdom"}]},{"given":"Conor","family":"McBride","sequence":"additional","affiliation":[{"name":"University of Strathclyde, Glasgow, United Kingdom"}]},{"given":"Peter","family":"Morris","sequence":"additional","affiliation":[{"name":"University of Nottingham, Nottingham, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2010,9,27]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_3"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005770"},{"key":"e_1_3_2_2_3_1","volume-title":"Generic Programming","author":"Altenkirch T.","year":"2002","unstructured":"}} T. Altenkirch and C. McBride . Generic programming within dependently typed programming . In Generic Programming , 2002 . }}T. Altenkirch and C. McBride. Generic programming within dependently typed programming. In Generic Programming, 2002."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/647849.737066"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_2_6_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_7_1","author":"Benke M.","year":"2003","unstructured":"}} M. Benke , P. Dybjer , and P. Jansson . Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing , 2003 . }}M. Benke, P. Dybjer, and P. Jansson. Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing, 2003.","journal-title":"Nordic Journal of Computing"},{"key":"e_1_3_2_2_8_1","unstructured":"}}E. Brady J. Chapman P.-E. Dagand A. Gundry C. McBride P. Morris and U. Norell. An Epigram implementation. }}E. Brady J. Chapman P.-E. Dagand A. Gundry C. McBride P. Morris and U. Norell. An Epigram implementation."},{"key":"e_1_3_2_2_9_1","volume-title":"TYPES","author":"Brady E.","year":"2003","unstructured":"}} E. Brady , C. McBride , and J. McKinna . Inductive families need not store their indices . In TYPES , 2003 . }}E. Brady, C. McBride, and J. McKinna. Inductive families need not store their indices. In TYPES, 2003."},{"key":"e_1_3_2_2_10_1","volume-title":"First-class phantom types. Technical report","author":"Cheney J.","year":"2003","unstructured":"}} J. Cheney and R. Hinze . First-class phantom types. Technical report , Cornell University , 2003 . }}J. Cheney and R. Hinze. First-class phantom types. Technical report, Cornell University, 2003."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00021-6"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/646529.695198"},{"key":"e_1_3_2_2_13_1","volume-title":"The Agda standard library","author":"Danielsson N. A.","year":"2010","unstructured":"}} N. A. Danielsson . The Agda standard library , 2010 . }}N. A. Danielsson. The Agda standard library, 2010."},{"key":"e_1_3_2_2_14_1","volume-title":"Logical Frameworks.","author":"Dybjer P.","year":"1991","unstructured":"}} P. Dybjer . Inductive sets and families in Martin-L\u00f6f's type theory. In Logical Frameworks. 1991 . }}P. Dybjer. Inductive sets and families in Martin-L\u00f6f's type theory. In Logical Frameworks. 1991."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/645894.671773"},{"key":"e_1_3_2_2_16_1","author":"Dybjer P.","year":"2000","unstructured":"}} P. Dybjer and A. Setzer . Induction-recursion and initial algebras. In Annals of Pure and Applied Logic , 2000 . }}P. Dybjer and A. Setzer. Induction-recursion and initial algebras. In Annals of Pure and Applied Logic, 2000.","journal-title":"Induction-recursion and initial algebras. In Annals of Pure and Applied Logic"},{"key":"e_1_3_2_2_17_1","volume-title":"Proof Theory in Computer Science.","author":"Dybjer P.","year":"2001","unstructured":"}} P. Dybjer and A. Setzer . Indexed induction-recursion . In Proof Theory in Computer Science. 2001 . }}P. Dybjer and A. Setzer. Indexed induction-recursion. In Proof Theory in Computer Science. 2001."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/949305.949317"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1754621.1754639"},{"key":"e_1_3_2_2_20_1","volume-title":"Algebra, Meaning and Computation.","author":"Goguen H.","year":"2006","unstructured":"}} H. Goguen , C. McBride , and J. McKinna . Eliminating dependent pattern matching . In Algebra, Meaning and Computation. 2006 . }}H. Goguen, C. McBride, and J. McKinna. Eliminating dependent pattern matching. In Algebra, Meaning and Computation. 2006."},{"key":"e_1_3_2_2_21_1","volume-title":"TAPSOFT'89","author":"Harper R.","unstructured":"}} R. Harper and R. Pollack . Type checking with universes . In TAPSOFT'89 . }}R. Harper and R. Pollack. Type checking with universes. In TAPSOFT'89."},{"key":"e_1_3_2_2_22_1","volume-title":"MPC.","author":"Hinze R.","year":"2000","unstructured":"}} R. Hinze . Polytypic values possess polykinded types . In MPC. 2000 . }}R. Hinze. Polytypic values possess polykinded types. In MPC. 2000."},{"key":"e_1_3_2_2_23_1","volume-title":"MPC","author":"Hinze R.","year":"2002","unstructured":"}} R. Hinze , J. Jeuring , and A. L\u00f6h . Type-indexed data types . In MPC , 2002 . }}R. Hinze, J. Jeuring, and A. L\u00f6h. Type-indexed data types. In MPC, 2002."},{"key":"e_1_3_2_2_24_1","volume-title":"Datatype-Generic Programming.","author":"Hinze R.","year":"2007","unstructured":"}} R. Hinze , J. Jeuring , and A. L\u00f6h . Comparing approaches to generic programming in Haskell . In Datatype-Generic Programming. 2007 . }}R. Hinze, J. Jeuring, and A. L\u00f6h. Comparing approaches to generic programming in Haskell. In Datatype-Generic Programming. 2007."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11783596_14"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263763"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604179"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596571"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and Reasoning","author":"Luo Z.","year":"1994","unstructured":"}} Z. Luo . Computation and Reasoning . Oxford University Press , 1994 . }}Z. Luo. Computation and Reasoning. Oxford University Press, 1994."},{"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_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.33"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_16"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006462"},{"key":"e_1_3_2_2_36_1","volume-title":"Master\u2019s thesis","author":"Norell U.","year":"2002","unstructured":"}} U. Norell . Functional generic programming and type theory. Master\u2019s thesis , Chalmers University of Technology , 2002 . }}U. Norell. Functional generic programming and type theory. Master\u2019s thesis, Chalmers University of Technology, 2002."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411213"},{"key":"e_1_3_2_2_39_1","volume-title":"ENS Lyon","author":"Paulin-Mohring C.","year":"1996","unstructured":"}} C. Paulin-Mohring . D\u00e9finitions inductives en th\u00e9orie des types d\u2019ordre sup\u00e9rieur. th\u00e8se d\u2019habilitation , ENS Lyon , 1996 . }}C. Paulin-Mohring. D\u00e9finitions inductives en th\u00e9orie des types d\u2019ordre sup\u00e9rieur. th\u00e8se d\u2019habilitation, ENS Lyon, 1996."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268967"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411301"},{"key":"e_1_3_2_2_42_1","unstructured":"}}The Coq Development Team. The Coq Proof Assistant Reference Manual. }}The Coq Development Team. The Coq Proof Assistant Reference Manual."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411318.1411326"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596614.1596616"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707790.1707799"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596585"}],"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 15th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1863543.1863547","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1863543.1863547","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:39:52Z","timestamp":1750232392000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1863543.1863547"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9,27]]},"references-count":45,"alternative-id":["10.1145\/1863543.1863547","10.1145\/1863543"],"URL":"https:\/\/doi.org\/10.1145\/1863543.1863547","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1932681.1863547","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010,9,27]]},"assertion":[{"value":"2010-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}