{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T19:56:15Z","timestamp":1730318175031,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,20]],"date-time":"2016-01-20T00:00:00Z","timestamp":1453248000000},"content-version":"vor","delay-in-days":9,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837660","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T14:05:00Z","timestamp":1452175500000},"page":"30-43","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["System f-omega with equirecursive types for datatype-generic programming"],"prefix":"10.1145","author":[{"given":"Yufei","family":"Cai","sequence":"first","affiliation":[{"name":"University of T\u00fcbingen, Germany"}]},{"given":"Paolo G.","family":"Giarrusso","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}]},{"given":"Klaus","family":"Ostermann","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"252","volume-title":"Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science","author":"Abadi M.","unstructured":"M. Abadi and M. P. Fiore . Syntactic considerations on recursive types . In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science , pages 242\u2013 252 . IEEE Computer Society, 1996. M. Abadi and M. P. Fiore. Syntactic considerations on recursive types. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, pages 242\u2013252. IEEE Computer Society, 1996."},{"key":"e_1_3_2_1_3_1","first-page":"257","volume-title":"Datatype-Generic Programming","author":"Altenkirch T.","unstructured":"T. Altenkirch , C. McBride , and P. Morris . Generic programming with dependent types . In Datatype-Generic Programming , pages 209\u2013 257 . Springer, 2007. Revised lectures of International Spring School SSDGP 2006. T. Altenkirch, C. McBride, and P. Morris. Generic programming with dependent types. In Datatype-Generic Programming, pages 209\u2013 257. Springer, 2007. Revised lectures of International Spring School SSDGP 2006."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"e_1_3_2_1_5_1","series-title":"Lecture Notes in Computer Science","first-page":"53","volume-title":"Mathematics of Program Construction","author":"Atanassow F.","unstructured":"F. Atanassow and J. Jeuring . Inferring Type Isomorphisms Generically . In D. Kozen, editor, Mathematics of Program Construction , volume 3125 of Lecture Notes in Computer Science , chapter 4, pages 32\u2013 53 . Springer Berlin \/ Heidelberg, 2004. F. Atanassow and J. Jeuring. Inferring Type Isomorphisms Generically. In D. Kozen, editor, Mathematics of Program Construction, volume 3125 of Lecture Notes in Computer Science, chapter 4, pages 32\u201353. Springer Berlin \/ Heidelberg, 2004."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/985799.985801"},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Pure and Applied Mathematics","first-page":"378","volume-title":"Logic and Algebra (Pontignano","author":"Berarducci A.","year":"1994","unstructured":"A. Berarducci . Infinite-calculus and non-sensible models . In A. Ursini and P. Agliano, editors, Logic and Algebra (Pontignano , 1994 ), volume 180 of Lecture Notes in Pure and Applied Mathematics , pages 339\u2013 378 . Marcel Dekker Inc., 1996. A. Berarducci. Infinite-calculus and non-sensible models. In A. Ursini and P. Agliano, editors, Logic and Algebra (Pontignano, 1994), volume 180 of Lecture Notes in Pure and Applied Mathematics, pages 339\u2013378. Marcel Dekker Inc., 1996."},{"key":"e_1_3_2_1_8_1","first-page":"6604","article-title":"Realizability and parametricity in pure type systems. In Foundations of Software Science and Computational Structures, pages 108\u2013122","author":"Bernardy J.-P.","year":"2011","unstructured":"J.-P. Bernardy and M. Lasson . Realizability and parametricity in pure type systems. In Foundations of Software Science and Computational Structures, pages 108\u2013122 . Springer LNCS 6604 , 2011 . J.-P. Bernardy and M. Lasson. Realizability and parametricity in pure type systems. In Foundations of Software Science and Computational Structures, pages 108\u2013122. Springer LNCS 6604, 2011.","journal-title":"Springer LNCS"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_2_1_10_1","volume-title":"Springer Berlin Heidelberg","author":"Bird R.","year":"1998","unstructured":"R. Bird and L. Meertens . Nested datatypes. In J. Jeuring, editor, Mathematics of Program Construction, number 1422 in Lecture Notes in Computer Science, pages 52\u201367 . Springer Berlin Heidelberg , 1998 . R. Bird and L. Meertens. Nested datatypes. In J. Jeuring, editor, Mathematics of Program Construction, number 1422 in Lecture Notes in Computer Science, pages 52\u201367. Springer Berlin Heidelberg, 1998."},{"key":"e_1_3_2_1_11_1","series-title":"Lecture Notes in Computer Science","first-page":"81","volume-title":"P. d","author":"Brandt M.","unstructured":"M. Brandt and F. Henglein . Coinductive axiomatization of recursive type equality and subtyping . In P. d . Groote and J. R. Hindley, editors, Typed Lambda Calculi and Applications , number 1210 in Lecture Notes in Computer Science , pages 63\u2013 81 . Springer Berlin Heidelberg, 1997. M. Brandt and F. Henglein. Coinductive axiomatization of recursive type equality and subtyping. In P. d. Groote and J. R. Hindley, editors, Typed Lambda Calculi and Applications, number 1210 in Lecture Notes in Computer Science, pages 63\u201381. Springer Berlin Heidelberg, 1997."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2379036.2379037"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006898"},{"key":"e_1_3_2_1_14_1","first-page":"438","volume-title":"Theoretical Aspects of Computer Software","author":"Bruce K. B.","unstructured":"K. B. Bruce , L. Cardelli , and B. C. Pierce . Comparing object encodings . In Theoretical Aspects of Computer Software , pages 415\u2013 438 . Springer, 1997. K. B. Bruce, L. Cardelli, and B. C. Pierce. Comparing object encodings. In Theoretical Aspects of Computer Software, pages 415\u2013438. Springer, 1997."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90020-3"},{"key":"e_1_3_2_1_16_1","first-page":"146","volume-title":"Proceedings of Symposium on Logic in Computer Science","author":"Colazzo D.","unstructured":"D. Colazzo and G. Ghelli . Subtyping recursive types in kernel Fun . In Proceedings of Symposium on Logic in Computer Science , pages 137\u2013 146 . IEEE, 1999. D. Colazzo and G. Ghelli. Subtyping recursive types in kernel Fun. In Proceedings of Symposium on Logic in Computer Science, pages 137\u2013146. IEEE, 1999."},{"first-page":"178","volume-title":"Rewriting and Typed Lambda Calculi","key":"e_1_3_2_1_17_1","unstructured":"\u0141. Czajka. A coinductive confluence proof for infinitary lambdacalculus . In Rewriting and Typed Lambda Calculi , pages 164\u2013 178 . Springer, 2014. \u0141. Czajka. A coinductive confluence proof for infinitary lambdacalculus. In Rewriting and Typed Lambda Calculi, pages 164\u2013178. Springer, 2014."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633628.2633634"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291196"},{"key":"e_1_3_2_1_20_1","unstructured":"J.\n Endrullis\n and \n A.\n Polonsky\n . \n Infinitary Rewriting Coinductively\n . In N. A. Danielsson and B. Nordstr\u00f6m editors 18th International Workshop on \n Types for Proofs and Programs (TYPES\n 2011\n ) volume \n 19\n of \n Leibniz International Proceedings in Informatics (LIPIcs) pages 16\u2013 \n 27\n . Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik 2013. J. Endrullis and A. Polonsky. Infinitary Rewriting Coinductively. In N. A. Danielsson and B. Nordstr\u00f6m editors 18th International Workshop on Types for Proofs and Programs (TYPES 2011) volume 19 of Leibniz International Proceedings in Informatics (LIPIcs) pages 16\u2013 27. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik 2013."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004318"},{"key":"e_1_3_2_1_22_1","volume-title":"ML Workshop","volume":"13","author":"Garrigue J.","year":"1998","unstructured":"J. Garrigue . Programming with polymorphic variants . In ML Workshop , volume 13 . Baltimore , 1998 . J. Garrigue. Programming with polymorphic variants. In ML Workshop, volume 13. Baltimore, 1998."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016872"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159861.1159863"},{"key":"e_1_3_2_1_25_1","volume-title":"Spring School on Datatype-Generic Programming","author":"Gibbons J.","year":"2007","unstructured":"J. Gibbons . Datatype-generic programming. In Spring School on Datatype-Generic Programming . Springer LNCS 4719, 2007 . J. Gibbons. Datatype-generic programming. In Spring School on Datatype-Generic Programming. Springer LNCS 4719, 2007."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007291"},{"key":"e_1_3_2_1_27_1","first-page":"161","volume-title":"Programming Languages and Systems","author":"Glew N.","unstructured":"N. Glew . A theory of second-order trees . In Programming Languages and Systems , pages 147\u2013 161 . Springer, 2002. N. Glew. A theory of second-order trees. In Programming Languages and Systems, pages 147\u2013161. Springer, 2002."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/648085.747179"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11783596_14"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002643"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_28"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.51"},{"key":"e_1_3_2_1_33_1","first-page":"49","volume-title":"Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming","volume":"76","author":"Jaskelioff M.","unstructured":"M. Jaskelioff and O. Rypacek . An investigation of the laws of traversals . In Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming , volume 76 , pages 40\u2013 49 . Open Publishing Association, 2012. M. Jaskelioff and O. Rypacek. An investigation of the laws of traversals. In Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming, volume 76, pages 40\u201349. Open Publishing Association, 2012."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00171-5"},{"key":"e_1_3_2_1_35_1","unstructured":"E. A. Kmett. The lens package. http:\/\/hackage.haskell.org\/ package\/lens. E. A. Kmett. The lens package. http:\/\/hackage.haskell.org\/ package\/lens."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604179"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_3_2_1_38_1","first-page":"523","article-title":"Functional programming with bananas, lenses, envelopes and barbed wire. In Functional Programming Languages and Computer Architecture, pages 124\u2013144","author":"Meijer E.","year":"1991","unstructured":"E. Meijer , M. Fokkinga , and R. Paterson . Functional programming with bananas, lenses, envelopes and barbed wire. In Functional Programming Languages and Computer Architecture, pages 124\u2013144 . Springer LNCS 523 , 1991 . E. Meijer, M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In Functional Programming Languages and Computer Architecture, pages 124\u2013144. Springer LNCS 523, 1991.","journal-title":"Springer LNCS"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291201.1291208"},{"key":"e_1_3_2_1_40_1","first-page":"266","volume-title":"Advanced Functional Programming","author":"Norell U.","unstructured":"U. Norell . Dependently typed programming in agda . In Advanced Functional Programming , pages 230\u2013 266 . Springer, 2009. Revised lectures of the 4th International School AFP 2002. U. Norell. Dependently typed programming in agda. In Advanced Functional Programming, pages 230\u2013266. Springer, 2009. Revised lectures of the 4th International School AFP 2002."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411203.1411213"},{"key":"e_1_3_2_1_42_1","volume-title":"Lecture notes on bidirectional type checking","author":"Pfenning F.","year":"2004","unstructured":"F. Pfenning . Lecture notes on bidirectional type checking . In Carnegie Mellon University course 15-312, \u201cFoundations of programming languages,\u201d fall 2004 . http:\/\/www.cs.cmu.edu\/~fp\/courses\/ 15312-f04\/handouts\/15-bidirectional.pdf, retrieved on 10 July 2015. F. Pfenning. Lecture notes on bidirectional type checking. In Carnegie Mellon University course 15-312, \u201cFoundations of programming languages,\u201d fall 2004. http:\/\/www.cs.cmu.edu\/~fp\/courses\/ 15312-f04\/handouts\/15-bidirectional.pdf, retrieved on 10 July 2015."},{"key":"e_1_3_2_1_43_1","volume-title":"Types and Programming Languages","author":"Pierce B. C.","year":"2002","unstructured":"B. C. Pierce . Types and Programming Languages . MIT Press , 2002 . B. C. Pierce. Types and Programming Languages. MIT Press, 2002."},{"key":"e_1_3_2_1_44_1","volume-title":"http:\/\/lists.seas.upenn.edu\/pipermail\/types-list\/ 2011\/001525.html","author":"Pottier F.","year":"2011","unstructured":"F. Pottier . {TYPES} System F omega with (equi-)recursive types. http:\/\/lists.seas.upenn.edu\/pipermail\/types-list\/ 2011\/001525.html , 2011 . Retrieved on 2 July 2015. F. Pottier. {TYPES} System F omega with (equi-)recursive types. http:\/\/lists.seas.upenn.edu\/pipermail\/types-list\/ 2011\/001525.html, 2011. Retrieved on 2 July 2015."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596585"},{"key":"e_1_3_2_1_46_1","volume-title":"Springer","author":"S\u00e9nizergues G.","year":"2001","unstructured":"G. S\u00e9nizergues . Some applications of the decidability of DPDA\u2019s equivalence. In Machines, Computations, and Universality, pages 114\u2013132 . Springer , 2001 . G. S\u00e9nizergues. Some applications of the decidability of DPDA\u2019s equivalence. In Machines, Computations, and Universality, pages 114\u2013132. Springer, 2001."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289460"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512765"},{"key":"e_1_3_2_1_49_1","volume-title":"Springer","author":"Stirling C.","year":"2002","unstructured":"C. Stirling . Deciding DPDA equivalence is primitive recursive. In Automata, languages and programming, pages 821\u2013832 . Springer , 2002 . C. Stirling. Deciding DPDA equivalence is primitive recursive. In Automata, languages and programming, pages 821\u2013832. Springer, 2002."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302457"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"],"location":"St. Petersburg FL USA","acronym":"POPL '16"},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837660","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T17:16:25Z","timestamp":1693847785000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837660"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":50,"alternative-id":["10.1145\/2837614.2837660","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837660","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837660","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}