{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:14Z","timestamp":1750306754444,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,24]],"date-time":"2013-09-24T00:00:00Z","timestamp":1379980800000},"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":[[2013,9,24]]},"DOI":"10.1145\/2502409.2502412","type":"proceedings-article","created":{"date-parts":[[2013,9,17]],"date-time":"2013-09-17T19:57:05Z","timestamp":1379447825000},"page":"25-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A multivalued language with a dependent type system"],"prefix":"10.1145","author":[{"given":"Neal","family":"Glew","sequence":"first","affiliation":[{"name":"Intel Labs, Santa Clara, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Sweeney","sequence":"additional","affiliation":[{"name":"Epic Games, Cary, NC, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leaf","family":"Petersen","sequence":"additional","affiliation":[{"name":"Intel Labs, Santa Clara, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,9,24]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"April","author":"Altenkirch T.","year":"2005","unstructured":"T. Altenkirch , C. McBride , and J. McKinna . Why dependent types matter. Manuscript, available online , April 2005 . T. Altenkirch, C. McBride, and J. McKinna. Why dependent types matter. Manuscript, available online, April 2005."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863560"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863587"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034788"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034789"},{"key":"e_1_3_2_1_9_1","volume-title":"July","author":"Glew N.","year":"2013","unstructured":"N. Glew , T. Sweeney , and L. Petersen . Formalising the \u03bb\u03c8 runtime. ArXiv e-prints , July 2013 . URL http:\/\/arxiv.org\/abs\/1307.5277. N. Glew, T. Sweeney, and L. Petersen. Formalising the \u03bb\u03c8 runtime. ArXiv e-prints, July 2013. URL http:\/\/arxiv.org\/abs\/1307.5277."},{"key":"e_1_3_2_1_10_1","unstructured":"INRIA. The Coq proof assistant. http:\/\/coq.inria.fr\/.  INRIA. The Coq proof assistant. http:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_11_1","series-title":"LNCS","volume-title":"CAV","author":"Jhala R.","year":"2011","unstructured":"R. Jhala , R. Majumdat , and A. Rybalchenko . HMC: Verifying functional programs using abstract interpreters . In CAV , volume 6806 of LNCS . Springer-Verlag , July 2011 . R. Jhala, R. Majumdat, and A. Rybalchenko. HMC: Verifying functional programs using abstract interpreters. In CAV, volume 6806 of LNCS. Springer-Verlag, July 2011."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411212"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103780"},{"key":"e_1_3_2_1_14_1","volume-title":"Sage: Unified hybrid checking for first-class types, general refinement types, and dynamic (extended report). Technical report","author":"Knowles K.","year":"2007","unstructured":"K. Knowles , A. Tomb , J. Gronski , S. Freund , and C. Flanagan . Sage: Unified hybrid checking for first-class types, general refinement types, and dynamic (extended report). Technical report , University of California at Santa Cruz , May 2007 . URL http:\/\/sage.soe.ucsc.edu\/. K. Knowles, A. Tomb, J. Gronski, S. Freund, and C. Flanagan. Sage: Unified hybrid checking for first-class types, general refinement types, and dynamic (extended report). Technical report, University of California at Santa Cruz, May 2007. URL http:\/\/sage.soe.ucsc.edu\/."},{"key":"e_1_3_2_1_15_1","volume-title":"Ontic: A Knowledge Representation System for Mathematics","author":"McAllester D.","year":"1989","unstructured":"D. McAllester . Ontic: A Knowledge Representation System for Mathematics . MIT Press , 1989 . D. McAllester. Ontic: A Knowledge Representation System for Mathematics. MIT Press, 1989."},{"key":"e_1_3_2_1_16_1","volume-title":"June","author":"McAllester D.","year":"1993","unstructured":"D. McAllester . The Ontic language. Available at http:\/\/ttic.uchicago.edu\/ dmcallester\/ontic-spec.ps , June 1993 . D. McAllester. The Ontic language. Available at http:\/\/ttic.uchicago.edu\/ dmcallester\/ontic-spec.ps, June 1993."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_1_19_1","unstructured":"U. Norell. Agda wiki. http:\/\/wiki.portal.chalmers.se\/agda\/.  U. Norell. Agda wiki. http:\/\/wiki.portal.chalmers.se\/agda\/."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869489"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500599"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"H.\n      Xi\n    .\n  Applied type system (extended abstract). In post-workshop proceedings of TYPES\n  2003 volume \n  3085\n   of \n  LNCS pages \n  394\n  --\n  408\n  . \n  Springer-Verlag 2004.  H. Xi. Applied type system (extended abstract). In post-workshop proceedings of TYPES 2003 volume 3085 of LNCS pages 394--408. Springer-Verlag 2004.","DOI":"10.1007\/978-3-540-24849-1_25"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"}],"event":{"name":"ICFP'13: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston Massachusetts USA","acronym":"ICFP'13"},"container-title":["Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2502409.2502412","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2502409.2502412","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:35Z","timestamp":1750231715000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2502409.2502412"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,24]]},"references-count":22,"alternative-id":["10.1145\/2502409.2502412","10.1145\/2502409"],"URL":"https:\/\/doi.org\/10.1145\/2502409.2502412","relation":{},"subject":[],"published":{"date-parts":[[2013,9,24]]},"assertion":[{"value":"2013-09-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}