乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T21:49:35Z","timestamp":1723758575771},"reference-count":47,"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":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["715753"],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002848","name":"Comisi\u00f3n Nacional de Investigaci\u00f3n Cient\u00edfica y Tecnol\u00f3gica","doi-asserted-by":"crossref","award":["1190058"],"id":[{"id":"10.13039\/501100002848","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"Dependent types help programmers write highly reliable code. However, this reliability comes at a cost: it can be challenging to write new prototypes in (or migrate old code to) dependently-typed programming languages. Gradual typing makes static type disciplines more flexible, so an appropriate notion of gradual dependent types could fruitfully lower this cost. However, dependent types raise unique challenges for gradual typing. Dependent typechecking involves the execution of program code, but gradually-typed code can signal runtime type errors or diverge. These runtime errors threaten the soundness guarantees that make dependent types so attractive, while divergence spoils the type-driven programming experience.<\/jats:p>\n \n This paper presents GDTL, a gradual dependently-typed language that emphasizes pragmatic dependently-typed programming. GDTL fully embeds both an untyped and dependently-typed language, and allows for smooth transitions between the two. In addition to gradual types we introduce\n gradual terms<\/jats:italic>\n , which allow the user to be imprecise in type indices and to omit proof terms; runtime checks ensure type safety. To account for nontermination and failure, we distinguish between compile-time normalization and run-time execution: compile-time normalization is\n approximate<\/jats:italic>\n but total, while runtime execution is\n exact<\/jats:italic>\n , but may fail or diverge. We prove that GDTL has decidable typechecking and satisfies all the expected properties of gradual languages. In particular, GDTL satisfies the static and dynamic gradual guarantees: reducing type precision preserves typedness, and altering type precision does not change program behavior outside of dynamic type failures. To prove these properties, we were led to establish a novel\n normalization gradual guarantee<\/jats:italic>\n that captures the monotonicity of approximate normalization with respect to imprecision.\n <\/jats:p>","DOI":"10.1145\/3341692","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-30","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Approximate normalization for gradual dependent types"],"prefix":"10.1145","volume":"3","author":[{"given":"Joseph","family":"Eremondi","sequence":"first","affiliation":[{"name":"University of British Columbia, Canada"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile \/ Inria, France"}]},{"given":"Ronald","family":"Garcia","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","article-title":"Gradual Type-and-Effect Systems","author":"Schwerter Felipe Ba\u00f1ados","year":"2016","journal-title":"Journal of Functional Programming 26"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","volume-title":"Interactive Theorem Proving and Program Development","author":"Bertot Yves","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_4_1","volume-title":"Types for Proofs and Programs","author":"Brady Edwin","year":"2003"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.5.639"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951933"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000011"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","volume-title":"Proving termination with multiset orderings","author":"Dershowitz Nachum","DOI":"10.1007\/3-540-09510-1_15"},{"key":"e_1_2_2_14_1","volume-title":"International Workshop on ProofSearch in Type Theories, PST T","volume":"10","author":"Eades Harley","year":"2010"},{"key":"e_1_2_2_15_1","unstructured":"Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. arXiv: cs.PL\/1610.07978 Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. arXiv: cs.PL\/1610.07978"},{"key":"e_1_2_2_16_1","volume-title":"Github Repository: GDTL-artifact. https:\/\/github.com\/JoeyEremondi\/GDTL- artifact\/ .","author":"Eremondi Joseph","year":"2019"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341692"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.22"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236766"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110282"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411212"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_2_2_27_1","first-page":"2","article-title":"A Tutorial Implementation of a Dependently Typed Lambda Calculus","volume":"102","author":"L\u00f6h Andres","year":"2010","journal-title":"Fundam. Inf."},{"key":"e_1_2_2_28_1","volume-title":"Equations for Hereditary Substitution in Leivant\u2019s Predicative System F: A Case Study. CoRR abs\/1508.00455","author":"Mangin Cyprien","year":"2015"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314643"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290327"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103779"},{"key":"e_1_2_2_34_1","volume-title":"Exploring New Frontiers of Theoretical Informatics, Jean-Jacques Levy, Ernst W","author":"Ou Xinming"},{"key":"e_1_2_2_35_1","volume-title":"Reasoning in Simple Type Theory \u2013 Festschrift in Honor of Peter B. Andrews on His 70th Birthday (Studies in Logic, Mathematical Logic and Foundations), Christoph Benzm\u00fcller, Chad Brown, J\u00f6rg Siekmann","author":"Pfenning Frank"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389469"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_29"},{"key":"e_1_2_2_39_1","volume-title":"CEFP 2007","author":"Sheard Tim","year":"2007"},{"key":"e_1_2_2_40_1","volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop. 81\u201392","author":"Jeremy"},{"key":"e_1_2_2_41_1","volume-title":"1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S","author":"Siek Jeremy G."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000053"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_2_2_46_1","unstructured":"Mat\u00edas Toro Elizabeth Labrada and \u00c9ric Tanter. 2018b. Gradual Parametricity Revisited. arXiv: cs.PL\/1807.04596 Mat\u00edas Toro Elizabeth Labrada and \u00c9ric Tanter. 2018b. Gradual Parametricity Revisited. arXiv: cs.PL\/1807.04596"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009849"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341692","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T07:47:59Z","timestamp":1672559279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341692"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":47,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341692"],"URL":"https:\/\/doi.org\/10.1145\/3341692","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}