{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:09:47Z","timestamp":1760044187214,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>Recent versions of the Haskell compiler GHC have a number of advanced features that allow many idioms from dependently typed programming to be encoded. We describe our experiences using this \"dependently typed Haskell\" to construct a performance-critical library that is a key component in a number of verification tools. We have discovered that it can be done, and it brings significant value, but also at a high cost. In this experience report, we describe the ways in which programming at the edge of what is expressible in Haskell's type system has brought us value, the difficulties that it has imposed, and some of the ways we coped with the difficulties.<\/jats:p>","DOI":"10.1145\/3341704","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Dependently typed Haskell in industry (experience report)"],"prefix":"10.1145","volume":"3","author":[{"given":"David Thrane","family":"Christiansen","sequence":"first","affiliation":[{"name":"Galois, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Iavor S.","family":"Diatchki","sequence":"additional","affiliation":[{"name":"Galois, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Dockins","sequence":"additional","affiliation":[{"name":"Galois, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joe","family":"Hendrix","sequence":"additional","affiliation":[{"name":"Galois, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tristan","family":"Ravitch","sequence":"additional","affiliation":[{"name":"Galois, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Silly Type Families. (September","author":"Augustsson Lennart","year":"1994","unstructured":"Lennart Augustsson and Kent Petersson . 1994. Silly Type Families. (September 1994 ). Unpublished draft. Lennart Augustsson and Kent Petersson. 1994. Silly Type Families. (September 1994). Unpublished draft."},{"volume-title":"Proof by Reflection","author":"Bertot Yves","key":"e_1_2_2_2_1","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2004. Proof by Reflection . Springer Berlin Heidelberg , Berlin, Heidelberg , 433\u2013448. Yves Bertot and Pierre Cast\u00e9ran. 2004. Proof by Reflection. Springer Berlin Heidelberg, Berlin, Heidelberg, 433\u2013448."},{"key":"e_1_2_2_3_1","unstructured":"Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroc\u0142aw Poland 53\u201364. https:\/\/hal.inria.fr\/hal-00790310 .  Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroc\u0142aw Poland 53\u201364. https:\/\/hal.inria.fr\/hal-00790310 ."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122967"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628141"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086397"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29613-5_6"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90066-B"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804307"},{"key":"e_1_2_2_10_1","volume-title":"VSTTE 2016","author":"Dockins Robert","year":"2016","unstructured":"Robert Dockins , Adam Foltzer , Joe Hendrix , Brian Huffman , Dylan McNamee , and Aaron Tomb . 2016 . Constructing Semantic Models of Programs with the Software Analysis Workbench. In Verified Software. Theories, Tools, and Experiments -8th International Conference , VSTTE 2016 , Toronto, ON, Canada , July 17-18, 2016, Revised Selected Papers. 56\u201372. Robert Dockins, Adam Foltzer, Joe Hendrix, Brian Huffman, Dylan McNamee, and Aaron Tomb. 2016. Constructing Semantic Models of Programs with the Software Analysis Workbench. In Verified Software. Theories, Tools, and Experiments -8th International Conference, VSTTE 2016, Toronto, ON, Canada, July 17-18, 2016, Revised Selected Papers. 56\u201372."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364522"},{"key":"e_1_2_2_12_1","unstructured":"GHC Issue #15186 2018. ghc#15186 8.4.2 panic in profiling build. https:\/\/ghc.haskell.org\/trac\/ghc\/ticket\/15186  GHC Issue #15186 2018. ghc#15186 8.4.2 panic in profiling build. https:\/\/ghc.haskell.org\/trac\/ghc\/ticket\/15186"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007291"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017481"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178246"},{"key":"e_1_2_2_16_1","volume-title":"IEEE Military Communications Conference, 2003. MILCOM 2003.","volume":"2","author":"Lewis J. R.","unstructured":"J. R. Lewis and B. Martin . 2003. Cryptol: high assurance, retargetable crypto development and validation . In IEEE Military Communications Conference, 2003. MILCOM 2003. , Vol. 2 . 820\u2013825. J. R. Lewis and B. Martin. 2003. Cryptol: high assurance, retargetable crypto development and validation. In IEEE Military Communications Conference, 2003. MILCOM 2003., Vol. 2. 820\u2013825."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503786"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_2_2_19_1","volume-title":"Proceedings of PICMET \u201914 Conference: Portland International Center for Management of Engineering and Technology; Infrastructure and Service Integration. 7\u201317","author":"McKinney Laura","year":"2014","unstructured":"Laura McKinney and Jef Bell . 2014 . The collaborative web: Building a divergent organizational model for research and development, based on 21st century notions of employee engagement . In Proceedings of PICMET \u201914 Conference: Portland International Center for Management of Engineering and Technology; Infrastructure and Service Integration. 7\u201317 . Laura McKinney and Jef Bell. 2014. The collaborative web: Building a divergent organizational model for research and development, based on 21st century notions of employee engagement. In Proceedings of PICMET \u201914 Conference: Portland International Center for Management of Engineering and Technology; Infrastructure and Service Integration. 7\u201317."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411215"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/636517.636528"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500599"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926411"},{"key":"e_1_2_2_27_1","unstructured":"Edward Z. Yang. 2017. Backpack: Towards Practical Mix-In Linking In Haskell. Ph.D. Dissertation. Stanford University.  Edward Z. Yang. 2017. Backpack: Towards Practical Mix-In Linking In Haskell. Ph.D. Dissertation. Stanford University."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103795"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341704","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341704","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:23Z","timestamp":1750207403000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341704"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":28,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341704"],"URL":"https:\/\/doi.org\/10.1145\/3341704","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}