{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T19:10:03Z","timestamp":1693854603256},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000005","name":"U.S. Department of Defense","doi-asserted-by":"publisher","award":["FA9550-16-1-0082"],"id":[{"id":"10.13039\/100000005","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1524519"],"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":[[2018,7,30]]},"abstract":"Dependently typed languages are well known for having a problem with code reuse. Traditional non-indexed algebraic datatypes (e.g. lists) appear alongside a plethora of indexed variations (e.g. vectors). Functions are often rewritten for both non-indexed and indexed versions of essentially the same datatype, which is a source of code duplication.<\/jats:p>\n We work in a Curry-style dependent type theory, where the same untyped term may be classified as both the non-indexed and indexed versions of a datatype. Many solutions have been proposed for the problem of dependently typed reuse, but we exploit Curry-style type theory in our solution to not only reuse data and programs, but do so at zero-cost (without a runtime penalty). Our work is an exercise in dependently typed generic programming, and internalizes the process of zero-cost reuse as the identity function in a Curry-style theory.<\/jats:p>","DOI":"10.1145\/3236799","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-30","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Generic zero-cost reuse for dependent types"],"prefix":"10.1145","volume":"2","author":[{"given":"Larry","family":"Diehl","sequence":"first","affiliation":[{"name":"University of Iowa, USA"}]},{"given":"Denis","family":"Firsov","sequence":"additional","affiliation":[{"name":"University of Iowa, USA"}]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[{"name":"University of Iowa, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"The implicit calculus of constructions as a programming language with dependent types. Foundations of Software Science and Computational Structures","author":"Barras Bruno","year":"2008","unstructured":"Bruno Barras and Bruno Bernardo . 2008. The implicit calculus of constructions as a programming language with dependent types. Foundations of Software Science and Computational Structures ( 2008 ), 365\u2013379. Bruno Barras and Bruno Bernardo. 2008. The implicit calculus of constructions as a programming language with dependent types. Foundations of Software Science and Computational Structures (2008), 365\u2013379."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500577"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000150"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364544"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951933"},{"key":"e_1_2_2_7_1","volume-title":"Foundations of dependent interoperability. Journal of Functional Programming 28","author":"Dagand Pierre-Evariste","year":"2018","unstructured":"Pierre-Evariste Dagand , Nicolas Tabareau , and \u00c9ric Tanter . 2018. Foundations of dependent interoperability. Journal of Functional Programming 28 ( 2018 ). Pierre-Evariste Dagand, Nicolas Tabareau, and \u00c9ric Tanter. 2018. Foundations of dependent interoperability. Journal of Functional Programming 28 (2018)."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_2_9_1","volume-title":"Zero-Cost Coercions for Program and Proof Reuse. (2018). arXiv","author":"Diehl Larry","year":"1802","unstructured":"Larry Diehl and Aaron Stump . 2018. Zero-Cost Coercions for Program and Proof Reuse. (2018). arXiv : 1802 .00787 Larry Diehl and Aaron Stump. 2018. Zero-Cost Coercions for Program and Proof Reuse. (2018). arXiv: 1802.00787"},{"key":"e_1_2_2_10_1","volume-title":"ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. 235\u2013252","author":"Firsov Denis","year":"2018","unstructured":"Denis Firsov , Richard Blair , and Aaron Stump . 2018 . Efficient Mendler-Style Lambda-Encodings in Cedille. In Interactive Theorem Proving - 9th International Conference , ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. 235\u2013252 . Denis Firsov, Richard Blair, and Aaron Stump. 2018. Efficient Mendler-Style Lambda-Encodings in Cedille. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. 235\u2013252."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167087"},{"key":"e_1_2_2_12_1","volume-title":"Reference: Racket. Technical Report PLT-TR-2010-1","author":"Flatt Matthew","year":"2010","unstructured":"Matthew Flatt and PLT. 2010 . Reference: Racket. Technical Report PLT-TR-2010-1 . PLT Design Inc . https:\/\/racket-lang.org\/tr1\/ . Matthew Flatt and PLT. 2010. Reference: Racket. Technical Report PLT-TR-2010-1. PLT Design Inc. https:\/\/racket-lang.org\/tr1\/ ."},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Herman Geuvers. 2001. Induction Is Not Derivable in Second Order Dependent Type Theory. In Typed Lambda Calculi and Applications (TLCA). 166\u2013181. Herman Geuvers. 2001. Induction Is Not Derivable in Second Order Dependent Type Theory. In Typed Lambda Calculi and Applications (TLCA). 166\u2013181.","DOI":"10.1007\/3-540-45413-6_16"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2502409.2502413"},{"key":"e_1_2_2_15_1","volume-title":"Dependent Intersection: A New Way of Defining Records in Type Theory. In 18th IEEE Symposium on Logic in Computer Science (LICS). 86\u201395","author":"Kopylov Alexei","year":"2003","unstructured":"Alexei Kopylov . 2003 . Dependent Intersection: A New Way of Defining Records in Type Theory. In 18th IEEE Symposium on Logic in Computer Science (LICS). 86\u201395 . Alexei Kopylov. 2003. Dependent Intersection: A New Way of Defining Records in Type Theory. In 18th IEEE Symposium on Logic in Computer Science (LICS). 86\u201395."},{"key":"e_1_2_2_16_1","unstructured":"Conor McBride. 2011. Ornamental algebras algebraic ornaments. (2011). Conor McBride. 2011. Ornamental algebras algebraic ornaments. (2011)."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"Alexandre Miquel. 2001. The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping. In Typed Lambda Calculi and Applications (TLCA) Samson Abramsky (Ed.). 344\u2013359. Alexandre Miquel. 2001. The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping. In Typed Lambda Calculi and Applications (TLCA) Samson Abramsky (Ed.). 344\u2013359.","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_2_2_20_1","volume-title":"International School on Advanced Functional Programming","author":"Norell Ulf","unstructured":"Ulf Norell . 2008. Dependently typed programming in Agda . In International School on Advanced Functional Programming . Springer , 230\u2013266. Ulf Norell. 2008. Dependently typed programming in Agda. In International School on Advanced Functional Programming. Springer, 230\u2013266."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000053"},{"key":"e_1_2_2_22_1","volume-title":"From Realizability to Induction via Dependent Intersection. Ann. Pure Appl. Logic","author":"Stump Aaron","year":"2018","unstructured":"Aaron Stump . 2018a. From Realizability to Induction via Dependent Intersection. Ann. Pure Appl. Logic ( 2018 ). to appear. Aaron Stump. 2018a. From Realizability to Induction via Dependent Intersection. Ann. Pure Appl. Logic (2018). to appear."},{"key":"e_1_2_2_23_1","volume-title":"Syntax and Semantics of Cedille. (2018). arXiv","author":"Stump Aaron","year":"1806","unstructured":"Aaron Stump . 2018b. Syntax and Semantics of Cedille. (2018). arXiv : 1806 .04709 Aaron Stump. 2018b. Syntax and Semantics of Cedille. (2018). arXiv: 1806.04709"},{"key":"e_1_2_2_24_1","unstructured":"The Coq Development Team. 2008. The Coq Proof Assistant Reference Manual. http:\/\/coq.inria.fr The Coq Development Team. 2008. The Coq Proof Assistant Reference Manual. http:\/\/coq.inria.fr"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00047-5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236799","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236799","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T19:48:32Z","timestamp":1672516112000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236799"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":24,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236799"],"URL":"http:\/\/dx.doi.org\/10.1145\/3236799","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}