{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:05Z","timestamp":1750221305545,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T00:00:00Z","timestamp":1515369600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1524519"],"award-info":[{"award-number":["1524519"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Department of Defense","award":["FA9550-16-1-0082"],"award-info":[{"award-number":["FA9550-16-1-0082"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,1,8]]},"DOI":"10.1145\/3167087","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"215-227","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Generic derivation of induction for impredicative encodings in Cedille"],"prefix":"10.1145","author":[{"given":"Denis","family":"Firsov","sequence":"first","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,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034807"},{"key":"e_1_3_2_1_2_1","volume-title":"Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT \u201911)","author":"Bahr Patrick","year":"2011","unstructured":"Patrick Bahr . 2011 . Evaluation \u00e0 la carte: Non-strict evaluation via compositional data types . In Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT \u201911) . 38\u201340. Patrick Bahr. 2011. Evaluation \u00e0 la carte: Non-strict evaluation via compositional data types. In Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT \u201911). 38\u201340."},{"key":"e_1_3_2_1_3_1","volume-title":"FroCoS 2017, Bras\u00edlia, Brazil, September 27-29, 2017, Proceedings (Lecture Notes in Computer Science), Clare Dixon and Marcelo Finger (Eds.)","volume":"10483","author":"Biendarra Julian","year":"2017","unstructured":"Julian Biendarra , Jasmin Christian Blanchette , Aymeric Bouzy , Martin Desharnais , Mathias Fleury , Johannes H\u00f6lzl , Ondrej Kuncar , Andreas Lochbihler , Fabian Meier , Lorenz Panny , Andrei Popescu , Christian Sternagel , Ren\u00e9 Thiemann , and Dmitriy Traytel . 2017 . Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. In Frontiers of Combining Systems - 11th International Symposium , FroCoS 2017, Bras\u00edlia, Brazil, September 27-29, 2017, Proceedings (Lecture Notes in Computer Science), Clare Dixon and Marcelo Finger (Eds.) , Vol. 10483 . Springer, 3\u201321. Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes H\u00f6lzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, Ren\u00e9 Thiemann, and Dmitriy Traytel. 2017. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. In Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Bras\u00edlia, Brazil, September 27-29, 2017, Proceedings (Lecture Notes in Computer Science), Clare Dixon and Marcelo Finger (Eds.), Vol. 10483. Springer, 3\u201321."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429094"},{"key":"e_1_3_2_1_5_1","unstructured":"The Agda development team. 2016. Agda. http:\/\/wiki.portal.chalmers. se\/agda\/pmwiki.php Version 2.5.1.  The Agda development team. 2016. Agda. http:\/\/wiki.portal.chalmers. se\/agda\/pmwiki.php Version 2.5.1."},{"key":"e_1_3_2_1_6_1","volume-title":"CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proceedings. 176\u2013191","author":"Fumex Cl\u00e9ment","year":"2011","unstructured":"Cl\u00e9ment Fumex , Neil Ghani , and Patricia Johann . 2011 . Indexed Induction and Coinduction, Fibrationally. In Algebra and Coalgebra in Computer Science - 4th International Conference , CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proceedings. 176\u2013191 . Cl\u00e9ment Fumex, Neil Ghani, and Patricia Johann. 2011. Indexed Induction and Coinduction, Fibrationally. In Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proceedings. 176\u2013191."},{"key":"e_1_3_2_1_7_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_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887459.1887488"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003500"},{"key":"e_1_3_2_1_10_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_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01110627"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1983.50"},{"key":"e_1_3_2_1_13_1","unstructured":"The Coq development team. 2016. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.fr Version 8.5.  The Coq development team. 2016. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.fr Version 8.5."},{"key":"e_1_3_2_1_14_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"},{"volume-title":"Programming with proofs: A second order type theory","author":"Parigot Michel","key":"e_1_3_2_1_15_1","unstructured":"Michel Parigot . 1988. Programming with proofs: A second order type theory . Springer Berlin Heidelberg , Berlin, Heidelberg , 145\u2013159. Michel Parigot. 1988. Programming with proofs: A second order type theory. Springer Berlin Heidelberg, Berlin, Heidelberg, 145\u2013159."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671440"},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of the Fifth Conference on the Mathematical Foundations of Programming Semantics","author":"Pfenning Frank","year":"1989","unstructured":"Frank Pfenning and Christine Paulin-Mohring . 1989 . Inductively Defined Types in the Calculus of Constructions . In Proceedings of the Fifth Conference on the Mathematical Foundations of Programming Semantics , Tulane University, New Orleans, Louisiana, M. Main, A. Melton, M. Mislove, and D. Schmidt (Eds.). Springer-Verlag LNCS 442, 209\u2013228. Frank Pfenning and Christine Paulin-Mohring. 1989. Inductively Defined Types in the Calculus of Constructions. In Proceedings of the Fifth Conference on the Mathematical Foundations of Programming Semantics, Tulane University, New Orleans, Louisiana, M. Main, A. Melton, M. Mislove, and D. Schmidt (Eds.). Springer-Verlag LNCS 442, 209\u2013228."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Aaron Stump. {n. d.}. The Calculus of Dependent Lambda Eliminations. Journal of Functional Programming 27 ({n. d.}) e14.  Aaron Stump. {n. d.}. The Calculus of Dependent Lambda Eliminations. Journal of Functional Programming 27 ({n. d.}) e14.","DOI":"10.1017\/S0956796817000053"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Aaron Stump. 2017. From Realizability to Induction via Dependent Intersection. Under consideration for Annals of Pure and Applied Logic.  Aaron Stump. 2017. From Realizability to Induction via Dependent Intersection. Under consideration for Annals of Pure and Applied Logic.","DOI":"10.1016\/j.apal.2018.03.002"},{"key":"e_1_3_2_1_20_1","volume-title":"Efficiency of lambda-encodings in total type theory. Journal of Functional Programming 26","author":"Stump Aaron","year":"2016","unstructured":"Aaron Stump and Peng Fu. 2016. Efficiency of lambda-encodings in total type theory. Journal of Functional Programming 26 ( 2016 ). Aaron Stump and Peng Fu. 2016. Efficiency of lambda-encodings in total type theory. Journal of Functional Programming 26 (2016)."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.75"},{"key":"e_1_3_2_1_23_1","first-page":"3","article-title":"Mendler-style Inductive Types, Categorically","volume":"6","author":"Uustalu Tarmo","year":"1999","unstructured":"Tarmo Uustalu and Varmo Vene . 1999 . Mendler-style Inductive Types, Categorically . Nordic J. of Computing 6 , 3 (Sept. 1999), 343\u2013361. Tarmo Uustalu and Varmo Vene. 1999. Mendler-style Inductive Types, Categorically. Nordic J. of Computing 6, 3 (Sept. 1999), 343\u2013361.","journal-title":"Nordic J. of Computing"},{"key":"e_1_3_2_1_24_1","unstructured":"Philip Wadler. 1990. Recursive types for free! http:\/\/homepages.inf.ed. ac.uk\/wadler\/papers\/free-rectypes\/free-rectypes.txt  Philip Wadler. 1990. Recursive types for free! http:\/\/homepages.inf.ed. ac.uk\/wadler\/papers\/free-rectypes\/free-rectypes.txt"},{"key":"e_1_3_2_1_25_1","unstructured":"Philip Wadler. 2016. The Expression Problem. http:\/\/homepages.inf.ed. ac.uk\/wadler\/papers\/expression\/expression.txt  Philip Wadler. 2016. The Expression Problem. http:\/\/homepages.inf.ed. ac.uk\/wadler\/papers\/expression\/expression.txt"}],"event":{"name":"CPP '18: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Los Angeles CA USA","acronym":"CPP '18"},"container-title":["Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167087","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167087","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167087","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:28Z","timestamp":1750212808000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167087"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":25,"alternative-id":["10.1145\/3167087","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167087","relation":{},"subject":[],"published":{"date-parts":[[2018,1,8]]},"assertion":[{"value":"2018-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}