{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:57:05Z","timestamp":1760043425146,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":62,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,8,9]],"date-time":"2020-08-09T00:00:00Z","timestamp":1596931200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1704041"],"award-info":[{"award-number":["1704041"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,8,27]]},"DOI":"10.1145\/3406088.3409015","type":"proceedings-article","created":{"date-parts":[[2020,7,31]],"date-time":"2020-07-31T04:08:01Z","timestamp":1596168481000},"page":"39-53","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Stitch: the sound type-indexed type checker (functional pearl)"],"prefix":"10.1145","author":[{"given":"Richard A.","family":"Eisenberg","sequence":"first","affiliation":[{"name":"Tweag I\/O, France \/ Bryn Mawr College, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,8,9]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236785"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018613"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_2_4_1","unstructured":"Lennart Augustsson and Magnus Carlsson. 1999. An exercise in dependent types: A well-typed interpreter. ( 1999 ). htp:\/\/citeseerx.ist.psu. edu\/viewdoc\/download?doi=10.1.1.39.2895& rep=rep1&type=pdf Unpublished manuscript."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122967"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Edwin Brady. 2013. Idris a general-purpose dependently typed programming language: Design and implementation. J. Funct. Prog. 23 ( 2013 ).","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_2_8_1","volume-title":"Simon Peyton Jones, and Stephanie Weirich","author":"Breitner Joachim","year":"2016","unstructured":"Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. 2016. Safe Zero-cost Coercions for Haskell. J. Funct. Program. 26 ( 2016 ), 1-79."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_3_2_2_10_1","volume-title":"Associated Type Synonyms. In International Conference on Functional Programming (ICFP '05)","author":"Chakravarty Manuel M. T.","year":"2005","unstructured":"Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyon Jones. 2005. Associated Type Synonyms. In International Conference on Functional Programming (ICFP '05). ACM."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/777388"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837665"},{"key":"e_1_3_2_2_14_1","volume-title":"Haskell Implementors Workshop","author":"Christiansen David Raymond","year":"2015","unstructured":"David Raymond Christiansen. 2015. A Pretty Printer that Says What it Means. Talk, Haskell Implementors Workshop, Vancouver, BC, Canada. htps:\/\/www.youtube.com\/watch?v=m7BBCcIDXSg"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Nicolaas Govert de Bruijn. 1972. Lambda calculus notation with nameless dummies a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75 5 ( 1972 ) 381-392. htps:\/\/doi.org\/10.1016\/ 1385-7258 ( 72 ) 90034-0","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_2_17_1","volume-title":"Simon Peyton Jones, and Stephanie Weirich","author":"Eisenberg Richard A.","year":"2014","unstructured":"Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. 2014. Closed Type Families with Overlapping Equations. In Principles of Programming Languages (POPL '14). ACM."},{"volume-title":"Dependently Typed Programming with Singletons. In ACM SIGPLAN Haskell Symposium.","author":"Richard","key":"e_1_3_2_2_18_1","unstructured":"Richard A. Eisenberg and Stephanie Weirich. 2012. Dependently Typed Programming with Singletons. In ACM SIGPLAN Haskell Symposium."},{"key":"e_1_3_2_2_19_1","volume-title":"Visible Type Application. In European Symposium on Programming (ESOP) (LNCS). Springer-Verlag.","author":"Eisenberg Richard A.","year":"2016","unstructured":"Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan Ahmed. 2016. Visible Type Application. In European Symposium on Programming (ESOP) (LNCS). Springer-Verlag."},{"key":"e_1_3_2_2_20_1","volume-title":"Pattern Guards and Transformational Patterns. In Haskell Workshop 2000 (haskell workshop 2000 ed.). htps:\/\/www.microsoft.com\/en-us\/research\/publication\/paternguards-and-transformational-paterns\/","author":"Erwig Martin","year":"2000","unstructured":"Martin Erwig and Simon Peyton Jones. 2000. Pattern Guards and Transformational Patterns. In Haskell Workshop 2000 (haskell workshop 2000 ed.). htps:\/\/www.microsoft.com\/en-us\/research\/publication\/paternguards-and-transformational-paterns\/"},{"key":"e_1_3_2_2_21_1","volume-title":"Suggesting Valid Hole Fits for Typed-Holes in Haskell. Master's thesis","author":"Gissurarson Matth\u00edas P\u00e1ll","year":"2018","unstructured":"Matth\u00edas P\u00e1ll Gissurarson. 2018. Suggesting Valid Hole Fits for Typed-Holes in Haskell. Master's thesis. Chalmers University of Technology, University of Gothenburg. htps:\/\/mpg.is\/papers\/ gissurarson2018suggesting-msc.pdf"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411218"},{"key":"e_1_3_2_2_24_1","unstructured":"Hiromi Ishii. 2014. Dependent Types in Haskell. School of Haskell blog. htps:\/\/www.schoolofhaskell.com\/user\/konn\/prove-yourhaskell-for-great-safety\/dependent-types-in-haskell"},{"volume-title":"Functional Programming with Overloading and Higher-Order Polymorphism","author":"Jones Mark P.","key":"e_1_3_2_2_25_1","unstructured":"Mark P. Jones. 1995. Functional Programming with Overloading and Higher-Order Polymorphism. In Advanced Functional Programming, Johan Jeuring and Erik Meijer (Eds.). LNCS, Vol. 925. Springer Verlag."},{"key":"e_1_3_2_2_26_1","volume-title":"Type Classes with Functional Dependencies. In European Symposium on Programming.","author":"Jones Mark P.","year":"2000","unstructured":"Mark P. Jones. 2000. Type Classes with Functional Dependencies. In European Symposium on Programming."},{"key":"e_1_3_2_2_27_1","volume-title":"GADTs meet their match. In International Conference on Functional Programming (ICFP '15)","author":"Karachalias Georgios","year":"2015","unstructured":"Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, and Simon Peyton Jones. 2015. GADTs meet their match. In International Conference on Functional Programming (ICFP '15). ACM."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604179"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"crossref","unstructured":"Ralf L\u00e4mmel and Simon Peyton Jones. 2005. Scrap Your Boilerplate With Class: Extensible Generic Functions. In ICFP.","DOI":"10.1145\/1086365.1086391"},{"key":"e_1_3_2_2_30_1","unstructured":"Justin Le. 2018. Introduction to Singletons. ( 2018 ). htps:\/\/blog.jle.im\/ entry\/introduction-to-singletons-3.html"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503786"},{"key":"e_1_3_2_2_33_1","unstructured":"Andres L\u00f6h. 2012. lhs2TeX. Haskell package. htps:\/\/www.andresloeh.de\/lhs2tex\/"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Pedro Magalh\u00e3es. 2012. The Right Kind of Generic Programming. ( 2012 ). To appear at WGP.","DOI":"10.1145\/2364394.2364397"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863523.1863529"},{"key":"e_1_3_2_2_36_1","unstructured":"Conor McBride. 2011. The Strathclyde Haskell Enhancement. htps: \/\/personal.cis.strath.ac.uk\/conor.mcbride\/pub\/she\/."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Stefan Monnier and David Haguenauer. 2010. Singleton types here singleton types there singleton types everywhere. In Programming languages meets program verification (PLPV '10). ACM.","DOI":"10.1145\/1707790.1707792"},{"volume-title":"Haskell Type Constraints Unleashed","author":"Orchard Dominic","key":"e_1_3_2_2_38_1","unstructured":"Dominic Orchard and Tom Schrijvers. 2010. Haskell Type Constraints Unleashed. In Functional and Logic Programming, Matthias Blume, Naoki Kobayashi, and Germ\u00e1n Vidal (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 56-71."},{"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","unstructured":"Simon Peyton Jones. 2003. Wearing the Hair Shirt: A Retrospective on Haskell. Invited talk at POPL."},{"key":"e_1_3_2_2_41_1","volume-title":"Haskell Workshop, John Launchbury (Ed.)","author":"Jones Simon Peyton","year":"1997","unstructured":"Simon Peyton Jones, Mark Jones, and Erik Meijer. 1997. Type classes: an exploration of the design space. In Haskell Workshop, John Launchbury (Ed.). Amsterdam, Netherlands."},{"key":"e_1_3_2_2_42_1","first-page":"636","article-title":"Unboxed values as ifrst class citizens","volume":"523","author":"Jones Simon Peyton","year":"1991","unstructured":"Simon Peyton Jones and John Launchbury. 1991. Unboxed values as ifrst class citizens. In FPCA (LNCS), Vol. 523. 636-666.","journal-title":"FPCA (LNCS)"},{"key":"e_1_3_2_2_43_1","unstructured":"Simon Peyton Jones and Mark Shields. 2004. Lexically-scoped type variables. ( 2004 ). htp:\/\/research.microsoft.com\/en-us\/um\/people\/ simonpj\/papers\/scoped-tyvars\/ Draft."},{"key":"e_1_3_2_2_44_1","volume-title":"Proceedings of the Haskell Workshop.","author":"Jones Simon Peyton","year":"2001","unstructured":"Simon Peyton Jones, Andrew Tolmach, and Tony Hoare. 2001. Playing by the Rules: Rewriting as a practical optimisation technique in GHC. In Proceedings of the Haskell Workshop."},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_3_2_2_46_1","volume-title":"International Conference on Functional Programming (ICFP '06)","author":"Jones Simon Peyton","year":"2006","unstructured":"Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geofrey Washburn. 2006. Simple unification-based type inference for GADTs. In International Conference on Functional Programming (ICFP '06). ACM."},{"volume-title":"A list of successes that can change the world","author":"Jones Simon Peyton","key":"e_1_3_2_2_48_1","unstructured":"Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, and Dimitrios Vytiniotis. 2016. A reflection on types. In A list of successes that can change the world. Springer. A festschrift in honor of Phil Wadler."},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-50940-2_46"},{"volume-title":"Pattern Synonyms. In ACM SIGPLAN Haskell Symposium. ACM.","author":"Pickering Matthew","key":"e_1_3_2_2_50_1","unstructured":"Matthew Pickering, Gerg\u0151 \u00c9rdi, Simon Peyton Jones, and Richard A. Eisenberg. 2016. Pattern Synonyms. In ACM SIGPLAN Haskell Symposium. ACM."},{"volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","key":"e_1_3_2_2_51_1","unstructured":"Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA."},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"volume-title":"Injective Type Families for Haskell. In Haskell Symposium (Haskell '15)","author":"Stolarek Jan","key":"e_1_3_2_2_53_1","unstructured":"Jan Stolarek, Simon Peyon Jones, and Richard A. Eisenberg. 2015. Injective Type Families for Haskell. In Haskell Symposium (Haskell '15). ACM."},{"volume-title":"Programs as Data Objects, Olivier Danvy and Andrzej Filinski (Eds.). LNCS","author":"Taha Walid","key":"e_1_3_2_2_54_1","unstructured":"Walid Taha, Henning Makholm, and John Hughes. 2001. Tag elimination and Jones-optimality. In Programs as Data Objects, Olivier Danvy and Andrzej Filinski (Eds.). LNCS, Vol. 2053. Springer Verlag."},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364524"},{"key":"e_1_3_2_2_56_1","volume-title":"Example: The Well-Typed Interpreter. The Idris Tutorial. htp:\/\/docs.idris-lang.org\/en\/latest\/tutorial\/interp.html","author":"Team The Idris","year":"2017","unstructured":"The Idris Team. 2017. Example: The Well-Typed Interpreter. The Idris Tutorial. htp:\/\/docs.idris-lang.org\/en\/latest\/tutorial\/interp.html"},{"key":"e_1_3_2_2_57_1","volume-title":"Simon Peyton Jones, and Tom Schrijvers","author":"Vytiniotis Dimitrios","year":"2010","unstructured":"Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers. 2010. Let Should Not Be Generalized. In Types in Language Design and Implementation (TLDI '10). ACM."},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41653"},{"volume-title":"System FC with Explicit Kind Equality. In International Conference on Functional Programming (ICFP '13)","author":"Weirich Stephanie","key":"e_1_3_2_2_60_1","unstructured":"Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. 2013. System FC with Explicit Kind Equality. In International Conference on Functional Programming (ICFP '13). ACM."},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009923"},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034818"},{"volume-title":"Types for Proofs and Programs","author":"Hongwei Xi.","key":"e_1_3_2_2_64_1","unstructured":"Hongwei Xi. 2004. Applied Type System. In Types for Proofs and Programs, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 394-408."},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"volume-title":"Coercion Quantification. In Haskell Implementors' Workshop.","author":"Xie Ningning","key":"e_1_3_2_2_66_1","unstructured":"Ningning Xie and Richard A. Eisenberg. 2018. Coercion Quantification. In Haskell Implementors' Workshop."},{"key":"e_1_3_2_2_67_1","volume-title":"Dimitrios Vytiniotis, and Jos\u00e9 Pedro Magalh\u00e3es.","author":"Yorgey Brent A.","year":"2012","unstructured":"Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and Jos\u00e9 Pedro Magalh\u00e3es. 2012. Giving Haskell a promotion. In Types in Language Design and Implementation (TLDI '12). ACM."}],"event":{"name":"ICFP '20: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual Event USA","acronym":"ICFP '20"},"container-title":["Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3406088.3409015","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3406088.3409015","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406088.3409015","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406088.3409015","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:52Z","timestamp":1750195912000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3406088.3409015"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,9]]},"references-count":62,"alternative-id":["10.1145\/3406088.3409015","10.1145\/3406088"],"URL":"https:\/\/doi.org\/10.1145\/3406088.3409015","relation":{},"subject":[],"published":{"date-parts":[[2020,8,9]]},"assertion":[{"value":"2020-08-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}