{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:15:56Z","timestamp":1781892956411,"version":"3.54.5"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T00:00:00Z","timestamp":1503964800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1521539,1319880"],"award-info":[{"award-number":["1521539,1319880"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2017,8,29]]},"abstract":"<jats:p>We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum dependent types. Our semantics consists of two related languages. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler's core language FC, is its explicitly-typed analogue, suitable for implementation in GHC. All of our results---chiefly, type safety, along with theorems that relate these two languages---have been formalized using the Coq proof assistant. Because our work is backwards compatible with Haskell, our type safety proof holds in the presence of nonterminating computation. However, unlike other full-spectrum dependently-typed languages, such as Coq, Agda or Idris, because of this nontermination, Haskell's term language does not correspond to a consistent logic.<\/jats:p>","DOI":"10.1145\/3110275","type":"journal-article","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T18:19:41Z","timestamp":1504030781000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["A specification for dependent types in Haskell"],"prefix":"10.1145","volume":"1","author":[{"given":"Stephanie","family":"Weirich","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antoine","family":"Voizard","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pedro Henrique Azevedo","family":"de Amorim","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique, France \/ University of Campinas, Brazil"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard A.","family":"Eisenberg","sequence":"additional","affiliation":[{"name":"Bryn Mawr College, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009861"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"David Aspinall and Martin Hoffman. 2005. Dependent Types. MIT Press 45\u201386. http:\/\/www.cis.upenn.edu\/~bcpierce\/attapl\/ David Aspinall and Martin Hoffman. 2005. Dependent Types. MIT Press 45\u201386. http:\/\/www.cis.upenn.edu\/~bcpierce\/attapl\/","DOI":"10.7551\/mitpress\/1104.003.0004"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_2_2_7_1","volume-title":"19th International Conference on Types for Proofs and Programs (TYPES","volume":"26","author":"Bezem Marc","year":"2014","unstructured":"Marc Bezem , Thierry Coquand , and Simon Huber . 2014 . A model of type theory in cubical sets . In 19th International Conference on Types for Proofs and Programs (TYPES 2013), Vol. 26 . 107\u2013128. Marc Bezem, Thierry Coquand, and Simon Huber. 2014. A model of type theory in cubical sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013), Vol. 26. 107\u2013128."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"e_1_2_2_10_1","volume-title":"a general-purpose dependently typed programming language: Design and implementation. J. Funct. Prog. 23","author":"Brady Edwin","year":"2013","unstructured":"Edwin Brady . 2013. Idris , a general-purpose dependently typed programming language: Design and implementation. J. Funct. Prog. 23 ( 2013 ). Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Prog. 23 (2013)."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628141"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086397"},{"key":"e_1_2_2_16_1","unstructured":"Coq development team. 2004. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.fr Version 8.0. Coq development team. 2004. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.fr Version 8.0."},{"key":"e_1_2_2_17_1","volume-title":"A Calculus of Constructions. (Nov","author":"Coquand Thierry","year":"1986","unstructured":"Thierry Coquand . 1986. A Calculus of Constructions. (Nov . 1986 ). manuscript. Thierry Coquand. 1986. A Calculus of Constructions. (Nov. 1986). manuscript."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603128"},{"key":"e_1_2_2_20_1","unstructured":"Haskell B. Curry J. Roger Hindley and J.P. Seldin (Eds.). 1972. Combinatory logic: Volume II. Amsterdam: North-Holland Pub. Co. Haskell B. Curry J. Roger Hindley and J.P. Seldin (Eds.). 1972. Combinatory logic: Volume II. Amsterdam: North-Holland Pub. Co."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_11"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062357"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_10"},{"key":"e_1_2_2_26_1","volume-title":"Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages","author":"Geuvers H.","unstructured":"H. Geuvers and F. Wiedijk . 2004. A logical framework with explicit conversions. In LFM\u201904 , Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages , Cork, Ireland, Carsten Schuermann (Ed.). 32\u201345. H. Geuvers and F. Wiedijk. 2004. A logical framework with explicit conversions. In LFM\u201904, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, Cork, Ireland, Carsten Schuermann (Ed.). 32\u201345."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"e_1_2_2_31_1","unstructured":"Chung-Kil Hur. 2010. Agda with the excluded middle is inconsistent? URL https:\/\/lists.chalmers.se\/pipermail\/agda\/2010\/ 001522.html .. (2010). Chung-Kil Hur. 2010. Agda with the excluded middle is inconsistent? URL https:\/\/lists.chalmers.se\/pipermail\/agda\/2010\/ 001522.html .. (2010)."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_2"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.2201\/NiiPi.2013.10.3"},{"key":"e_1_2_2_34_1","unstructured":"Per Martin-L\u00f6f. 1971. A Theory of Types. (1971). Unpublished manuscript. Per Martin-L\u00f6f. 1971. A Theory of Types. (1971). Unpublished manuscript."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_2_2_36_1","volume-title":"Studies in Proof Theory","volume":"1","author":"Martin-L\u00f6f Per","year":"1984","unstructured":"Per Martin-L\u00f6f . 1984 . Intuitionistic type theory . Studies in Proof Theory , Vol. 1 . Bibliopolis. iv+91 pages. Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Studies in Proof Theory, Vol. 1. Bibliopolis. iv+91 pages."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_13"},{"key":"e_1_2_2_38_1","unstructured":"Conor McBride. 2004. Epigram. (2004). http:\/\/www.dur.ac.uk\/CARG\/epigram . Conor McBride. 2004. Epigram. (2004). http:\/\/www.dur.ac.uk\/CARG\/epigram ."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_2_2_40_1","volume-title":"Re: Agda with the excluded middle is inconsistent? URL https:\/\/lists.chalmers.se\/pipermail\/agda\/ 2010\/001543.html .","author":"Miquel Alexandre","year":"2010","unstructured":"Alexandre Miquel . 2010 . Re: Agda with the excluded middle is inconsistent? URL https:\/\/lists.chalmers.se\/pipermail\/agda\/ 2010\/001543.html . (2010). Alexandre Miquel. 2010. Re: Agda with the excluded middle is inconsistent? URL https:\/\/lists.chalmers.se\/pipermail\/agda\/ 2010\/001543.html . (2010)."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932499"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411215"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676974"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804314"},{"key":"e_1_2_2_53_1","volume-title":"The Calculus of Dependent Lambda Eliminations. (Sept","author":"Stump Aaron","year":"2016","unstructured":"Aaron Stump . 2016. The Calculus of Dependent Lambda Eliminations. (Sept . 2016 ). http:\/\/homepage.cs.uiowa.edu\/~astump\/ papers\/cedille- draft.pdf Submitted for publication. Aaron Stump. 2016. The Calculus of Dependent Lambda Eliminations. (Sept. 2016). http:\/\/homepage.cs.uiowa.edu\/~astump\/ papers\/cedille- draft.pdf Submitted for publication."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503887.2503890"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411246"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500599"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00047-5"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_14"},{"key":"e_1_2_2_62_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\/3110275","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110275","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110275","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110275"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,29]]},"references-count":50,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2017,8,29]]}},"alternative-id":["10.1145\/3110275"],"URL":"https:\/\/doi.org\/10.1145\/3110275","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,29]]},"assertion":[{"value":"2017-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}