{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:59Z","timestamp":1772164019672,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["ERC Advanced Grant ProofCert"],"award-info":[{"award-number":["ERC Advanced Grant ProofCert"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009841","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"387-399","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["The exp-log normal form of types: decomposing extensional equality and representing terms compactly"],"prefix":"10.1145","author":[{"given":"Danko","family":"Ilik","sequence":"first","affiliation":[{"name":"Trusted Labs, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Manuscript","author":"Ahmad A.","year":"2010","unstructured":"A. Ahmad , D. Licata , and R. Harper . Deciding coproduct equality with focusing . Manuscript , 2010 . A. Ahmad, D. Licata, and R. Harper. Deciding coproduct equality with focusing. Manuscript, 2010."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871869"},{"key":"e_1_3_2_1_3_1","first-page":"20","volume-title":"Workshop on Normalization by Evaluation","author":"Balat V.","year":"2009","unstructured":"V. Balat . Keeping sums under control . In Workshop on Normalization by Evaluation , pages 11\u2013 20 , Los Angeles, United States , Aug. 2009 . V. Balat. Keeping sums under control. In Workshop on Normalization by Evaluation, pages 11\u201320, Los Angeles, United States, Aug. 2009."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964007"},{"key":"e_1_3_2_1_5_1","volume-title":"An intuitionistic formula hierarchy based on high-school identities. arXiv:1601.04876","author":"Brock-Nannestad T.","year":"2016","unstructured":"T. Brock-Nannestad and D. Ilik . An intuitionistic formula hierarchy based on high-school identities. arXiv:1601.04876 , 2016 . T. Brock-Nannestad and D. Ilik. An intuitionistic formula hierarchy based on high-school identities. arXiv:1601.04876, 2016."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00012-004-1900-2"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"R.\n      Di Cosmo\n     and \n      D.\n      Kesner\n  . \n  A confluent reduction for the extensional typed \u03bb-calculus with pairs sums recursion and terminal object\n  . In A. Lingas R. Karlsson and S. Carlsson editors Automata Languages\n  and Programming volume \n  700\n   of \n  Lecture Notes in Computer Science pages 645\u2013\n  656\n  . Springer Berlin Heidelberg 1993.   R. Di Cosmo and D. Kesner. A confluent reduction for the extensional typed \u03bb-calculus with pairs sums recursion and terminal object. In A. Lingas R. Karlsson and S. Carlsson editors Automata Languages and Programming volume 700 of Lecture Notes in Computer Science pages 645\u2013656. Springer Berlin Heidelberg 1993.","DOI":"10.1007\/3-540-56939-1_109"},{"key":"e_1_3_2_1_8_1","volume-title":"Simply typed lambda-calculus modulo type isomorphisms. Draft at https:\/\/hal.inria.fr\/hal-01109104","author":"D\u00b4\u0131az-Caro A.","year":"2015","unstructured":"A. D\u00b4\u0131az-Caro and G. Dowek . Simply typed lambda-calculus modulo type isomorphisms. Draft at https:\/\/hal.inria.fr\/hal-01109104 , 2015 . A. D\u00b4\u0131az-Caro and G. Dowek. Simply typed lambda-calculus modulo type isomorphisms. Draft at https:\/\/hal.inria.fr\/hal-01109104, 2015."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2897336.2897346"},{"key":"e_1_3_2_1_10_1","first-page":"151","volume-title":"Rewriting Techniques and Applications","author":"Dougherty D.","unstructured":"D. Dougherty . Some lambda calculi with categorical sums and products . In Rewriting Techniques and Applications , pages 137\u2013 151 . Springer, 1993. D. Dougherty. Some lambda calculi with categorical sums and products. In Rewriting Techniques and Applications, pages 137\u2013151. Springer, 1993."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/788017.788746"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2005.09.001"},{"key":"e_1_3_2_1_13_1","series-title":"Lecture Notes in Mathematics","first-page":"37","volume-title":"Logic Colloquium \u201973","author":"Friedman H.","unstructured":"H. Friedman . Equality between functionals . In Logic Colloquium \u201973 , volume 453 of Lecture Notes in Mathematics , pages 22\u2013 37 . Springer, 1975. H. Friedman. Equality between functionals. In Logic Colloquium \u201973, volume 453 of Lecture Notes in Mathematics, pages 22\u201337. Springer, 1975."},{"key":"e_1_3_2_1_14_1","first-page":"185","volume-title":"Typed Lambda Calculi and Applications","author":"Ghani N.","unstructured":"N. Ghani . \u03b2\u03b7-equality for coproducts . In Typed Lambda Calculi and Applications , pages 171\u2013 185 . Springer, 1995. N. Ghani. \u03b2\u03b7-equality for coproducts. In Typed Lambda Calculi and Applications, pages 171\u2013185. Springer, 1995."},{"key":"e_1_3_2_1_15_1","volume-title":"Orders of Infinity. The \u2018Infinit\u00e4rcalc\u00fcl","author":"Hardy G. H.","year":"1910","unstructured":"G. H. Hardy . Orders of Infinity. The \u2018Infinit\u00e4rcalc\u00fcl \u2019 of Paul Du Bois-Reymond. Cambridge Tracts in Mathematic and Mathematical Physics. Cambridge University Press , 1910 . G. H. Hardy. Orders of Infinity. The \u2018Infinit\u00e4rcalc\u00fcl\u2019 of Paul Du Bois-Reymond. Cambridge Tracts in Mathematic and Mathematical Physics. Cambridge University Press, 1910."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603115"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392389.2392432"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000006X"},{"key":"e_1_3_2_1_19_1","first-page":"331","volume-title":"13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs)","author":"Scherer G.","year":"2015","unstructured":"G. Scherer . Multi-Focusing on Extensional Rewriting with Sums. In T. Altenkirch, editor , 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 317\u2013 331 , Dagstuhl, Germany , 2015 . Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik. ISBN 978-3- 939897-87-3. Introduction The exp-log Normal Form of Types -Congruence Classes at ENF Type A Compact Representation of Terms at ENF Type A Converter for the Compact Term Representation Conclusion G. Scherer. Multi-Focusing on Extensional Rewriting with Sums. In T. Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 317\u2013331, Dagstuhl, Germany, 2015. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik. ISBN 978-3- 939897-87-3. Introduction The exp-log Normal Form of Types -Congruence Classes at ENF Type A Compact Representation of Terms at ENF Type A Converter for the Compact Term Representation Conclusion"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009841","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009841","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:21Z","timestamp":1750203381000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009841"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":19,"alternative-id":["10.1145\/3009837.3009841","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009841","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009841","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}