{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:23Z","timestamp":1772164043055,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,9,9]],"date-time":"2012-09-09T00:00:00Z","timestamp":1347148800000},"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":[[2012,9,9]]},"DOI":"10.1145\/2364527.2364554","type":"proceedings-article","created":{"date-parts":[[2012,9,12]],"date-time":"2012-09-12T09:01:27Z","timestamp":1347440487000},"page":"341-352","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Equality proofs and deferred type errors"],"prefix":"10.1145","author":[{"given":"Dimitrios","family":"Vytiniotis","sequence":"first","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Peyton Jones","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9 Pedro","family":"Magalh\u00e3es","sequence":"additional","affiliation":[{"name":"Utrecht University, Utrecht, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,9,9]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"57","volume-title":"14th International Conference, FOSSACS 2011","author":"Abel Andreas","year":"2011","unstructured":"Andreas Abel . Irrelevance in type theory with a heterogeneous equality judgement. In phFoundations of Software Science and Computational Structures , 14th International Conference, FOSSACS 2011 , pages 57 -- 71 . Springer , 2011 . Andreas Abel. Irrelevance in type theory with a heterogeneous equality judgement. In phFoundations of Software Science and Computational Structures, 14th International Conference, FOSSACS 2011, pages 57--71. Springer, 2011."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_3_2_1_3_1","first-page":"365","volume-title":"The implicit calculus of constructions as a programming language with dependent types. In phFoundations of Software Science and Computation Structure","author":"Barras Bruno","year":"2008","unstructured":"Bruno Barras and Bruno Bernardo . The implicit calculus of constructions as a programming language with dependent types. In phFoundations of Software Science and Computation Structure , pages 365 -- 379 , 2008 . 10.1007\/978--3--540--78499--9_26. Bruno Barras and Bruno Bernardo. The implicit calculus of constructions as a programming language with dependent types. In phFoundations of Software Science and Computation Structure, pages 365--379, 2008. 10.1007\/978--3--540--78499--9_26."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985864"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.27"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929529.1929532"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Edwin\n      Brady Conor\n      McBride and \n      James\n      McKinna\n    .\n  Inductive families need not store their indices\n  . In Stefano Berardi Mario Coppo and Ferruccio Damiani editors phTYPES volume \n  3085\n   of \n  phLecture Notes in Computer Science pages \n  115\n  --\n  129\n  . \n  Springer 2003\n  .  Edwin Brady Conor McBride and James McKinna. Inductive families need not store their indices. In Stefano Berardi Mario Coppo and Ferruccio Damiani editors phTYPES volume 3085 of phLecture Notes in Computer Science pages 115--129. Springer 2003.","DOI":"10.1007\/978-3-540-24849-1_8"},{"key":"e_1_3_2_1_9_1","unstructured":"chak  chak"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086397"},{"key":"e_1_3_2_1_11_1","volume-title":"First-class phantom types. CUCIS TR2003--1901","author":"Cheney James","year":"2003","unstructured":"James Cheney and Ralf Hinze . First-class phantom types. CUCIS TR2003--1901 , Cornell University , 2003 . James Cheney and Ralf Hinze. First-class phantom types. CUCIS TR2003--1901, Cornell University, 2003."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_3_2_1_13_1","volume-title":"Scaling up: The very busy background compiler. phMSDN Magazine, 6","author":"Gertz Matthew","year":"2005","unstructured":"Matthew Gertz . Scaling up: The very busy background compiler. phMSDN Magazine, 6 2005 . URL http:\/\/msdn.microsoft.com\/en-us\/magazine\/cc163781.aspx. Matthew Gertz. Scaling up: The very busy background compiler. phMSDN Magazine, 6 2005. URL http:\/\/msdn.microsoft.com\/en-us\/magazine\/cc163781.aspx."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.01.004"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"e_1_3_2_1_16_1","first-page":"301","volume-title":"Simon Peyton Jones, and Chung-chieh Shan. Fun with type functions","author":"Kiselyov Oleg","year":"2010","unstructured":"and Shan}Kiselyov09funwith Oleg Kiselyov , Simon Peyton Jones, and Chung-chieh Shan. Fun with type functions . In A.W. Roscoe, Cliff B. Jones, and Kenneth R. Wood, editors, phReflections on the Work of C.A.R. Hoare, History of Computing, pages 301 -- 331 . Springer London , 2010 . 10.1007\/978--1--84882--912--1_14. and Shan}Kiselyov09funwithOleg Kiselyov, Simon Peyton Jones, and Chung-chieh Shan. Fun with type functions. In A.W. Roscoe, Cliff B. Jones, and Kenneth R. Wood, editors, phReflections on the Work of C.A.R. Hoare, History of Computing, pages 301--331. Springer London, 2010. 10.1007\/978--1--84882--912--1_14."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086391"},{"key":"e_1_3_2_1_18_1","volume-title":"Licata and Robert Harper. A formulation of dependent ML with explicit equality proofs","author":"Daniel","year":"2005","unstructured":"Daniel R. Licata and Robert Harper. A formulation of dependent ML with explicit equality proofs . Technical Report Carnegie Mellon University-CS-05--178, Carnegie Mellon University Department of Computer Science , 2005 . Daniel R. Licata and Robert Harper. A formulation of dependent ML with explicit equality proofs. Technical Report Carnegie Mellon University-CS-05--178, Carnegie Mellon University Department of Computer Science, 2005."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103697"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006804"},{"key":"e_1_3_2_1_21_1","first-page":"344","volume-title":"TLCA'01","author":"Miquel Alexandre","year":"2001","unstructured":"Alexandre Miquel . The implicit calculus of constructions: extending pure type systems with an intersection type binder and subtyping. In phProceedings of the 5th International Conference on Typed Lambda Calculi and Applications , TLCA'01 , pages 344 -- 359 , Berlin, Heidelberg , 2001 . Springer-Verlag . ISBN 3--540--41960--8. Alexandre Miquel. The implicit calculus of constructions: extending pure type systems with an intersection type binder and subtyping. In phProceedings of the 5th International Conference on Typed Lambda Calculi and Applications, TLCA'01, pages 344--359, Berlin, Heidelberg, 2001. Springer-Verlag. ISBN 3--540--41960--8."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Nathan\n      Mishra-Linger\n     and \n      Tim\n      Sheard\n    .\n  Erasure and polymorphism in pure type systems\n  . In Roberto Amadio editor phFoundations of Software Science and Computational Structures volume \n  4962\n   of \n  phLecture Notes in Computer Science pages \n  350\n  --\n  364\n  . \n  Springer Berlin \/ Heidelberg 2008\n  .   Nathan Mishra-Linger and Tim Sheard. Erasure and polymorphism in pure type systems. In Roberto Amadio editor phFoundations of Software Science and Computational Structures volume 4962 of phLecture Notes in Computer Science pages 350--364. Springer Berlin \/ Heidelberg 2008.","DOI":"10.1007\/978-3-540-78499-9_25"},{"key":"e_1_3_2_1_24_1","unstructured":"nd Launchbury(1991)}peyton-jones  nd Launchbury(1991)}peyton-jones"},{"key":"e_1_3_2_1_25_1","first-page":"636","volume-title":"Unboxed values as first class citizens in a non-strict functional programming language. In phFPCA91: Conference on Functional Programming Languages and Computer Architecture","author":"Jones Simon Peyton","year":"1991","unstructured":":unboxed Simon Peyton Jones and John Launchbury . Unboxed values as first class citizens in a non-strict functional programming language. In phFPCA91: Conference on Functional Programming Languages and Computer Architecture , pages 636 -- 666 , New York, NY , August 1991 . ACM Press . :unboxedSimon Peyton Jones and John Launchbury. Unboxed values as first class citizens in a non-strict functional programming language. In phFPCA91: Conference on Functional Programming Languages and Computer Architecture, pages 636--666, New York, NY, August 1991. ACM Press."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(97)00029-4"},{"key":"e_1_3_2_1_27_1","unstructured":"t al.(2006)Peyton Jones Vytiniotis Weirich and Washburn}spj  t al.(2006)Peyton Jones Vytiniotis Weirich and Washburn}spj"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_3_2_1_29_1","unstructured":"t al.(2007)Peyton Jones Vytiniotis Weirich and Shields}peyton-jones  t al.(2007)Peyton Jones Vytiniotis Weirich and Shields}peyton-jones"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_2_1_32_1","first-page":"389","volume-title":"The essence of ML type inference","author":"Pottier Fran\u00e7ois","year":"2005","unstructured":"y(2005)}pottier:pierce-chapter Fran\u00e7ois Pottier and Didier R\u00e9my . The essence of ML type inference . In Benjamin C. Pierce, editor, phAdvanced Topics in Types and Programming Languages, chapter 10, pages 389 -- 489 . MIT Press , 2005 . y(2005)}pottier:pierce-chapterFran\u00e7ois Pottier and Didier R\u00e9my. The essence of ML type inference. In Benjamin C. Pierce, editor, phAdvanced Topics in Types and Programming Languages, chapter 10, pages 389--489. MIT Press, 2005."},{"key":"e_1_3_2_1_33_1","first-page":"106","volume-title":"Meta-programming with built-in type equality. In phProc 4th International Workshop on Logical Frameworks and Meta-languages (LFM'04)","author":"Sheard Tim","year":"2004","unstructured":"Tim Sheard and Emir Pasalic . Meta-programming with built-in type equality. In phProc 4th International Workshop on Logical Frameworks and Meta-languages (LFM'04) , pages 106 -- 124 , July 2004 . Tim Sheard and Emir Pasalic. Meta-programming with built-in type equality. In phProc 4th International Workshop on Logical Frameworks and Meta-languages (LFM'04), pages 106--124, July 2004."},{"key":"e_1_3_2_1_34_1","first-page":"81","volume-title":"Siek and Walid Taha. Gradual typing for functional languages. In phScheme and Functional Programming Workshop","author":"Jeremy","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In phScheme and Functional Programming Workshop , pages 81 -- 92 , September 2006 . Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In phScheme and Functional Programming Workshop, pages 81--92, September 2006."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1408681.1408688"},{"key":"e_1_3_2_1_36_1","unstructured":"and Donnelly}sulzmann  and Donnelly}sulzmann"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596598"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_3_2_1_40_1","unstructured":"}coqThe Coq Team. phCoq. URL http:\/\/coq.inria.fr.  }coqThe Coq Team. phCoq. URL http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926411"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/239912.239917"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103795"}],"event":{"name":"ICFP'12: ACM SIGPLAN International Conference on Functional Programming","location":"Copenhagen Denmark","acronym":"ICFP'12","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 17th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2364527.2364554","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2364527.2364554","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:34:00Z","timestamp":1750224840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2364527.2364554"}},"subtitle":["a compiler pearl"],"short-title":[],"issued":{"date-parts":[[2012,9,9]]},"references-count":44,"alternative-id":["10.1145\/2364527.2364554","10.1145\/2364527"],"URL":"https:\/\/doi.org\/10.1145\/2364527.2364554","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2398856.2364554","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2012,9,9]]},"assertion":[{"value":"2012-09-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}