{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T00:41:05Z","timestamp":1768696865248,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":50,"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":[{"name":"NWO","award":["14319"],"award-info":[{"award-number":["14319"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,1,8]]},"DOI":"10.1145\/3167085","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"201-214","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Finite sets in homotopy type theory"],"prefix":"10.1145","author":[{"given":"Dan","family":"Frumin","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}]},{"given":"Herman","family":"Geuvers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}]},{"given":"L\u00e9on","family":"Gondelman","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}]},{"given":"Niels van der","family":"Weide","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2018,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. CoRR abs\/1610.00026","author":"Adams Robin","year":"2016","unstructured":"Robin Adams , Marc Bezem , and Thierry Coquand . 2016. A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. CoRR abs\/1610.00026 ( 2016 ). http:\/\/arxiv.org\/abs\/1610.00026 Robin Adams, Marc Bezem, and Thierry Coquand. 2016. A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. CoRR abs\/1610.00026 (2016). http:\/\/arxiv.org\/abs\/1610.00026"},{"key":"e_1_3_2_2_2_1","volume-title":"Quotient Inductive-Inductive Types. CoRR abs\/1612.02346","author":"Altenkirch Thorsten","year":"2016","unstructured":"Thorsten Altenkirch , Paolo Capriotti , Gabe Dijkstra , and Fredrik Nordvall Forsberg . 2016. Quotient Inductive-Inductive Types. CoRR abs\/1612.02346 ( 2016 ). http:\/\/arxiv.org\/abs\/1612.02346 Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, and Fredrik Nordvall Forsberg. 2016. Quotient Inductive-Inductive Types. CoRR abs\/1612.02346 (2016). http:\/\/arxiv.org\/abs\/1612.02346"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_31"},{"key":"e_1_3_2_2_4_1","volume-title":"1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016","author":"Altenkirch Thorsten","year":"2016","unstructured":"Thorsten Altenkirch and Ambrus Kaposi . 2016 . Normalisation by Evaluation for Dependent Types . In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 , June 22-26, 2016, Porto, Portugal. 6:1\u20136:16. Thorsten Altenkirch and Ambrus Kaposi. 2016. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal. 6:1\u20136:16."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000198"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.21"},{"key":"e_1_3_2_2_8_1","first-page":"1","article-title":"Higher Inductive Types in Programming","volume":"23","author":"Basold Henning","year":"2017","unstructured":"Henning Basold , Herman Geuvers , and Niels van der Weide . 2017 . Higher Inductive Types in Programming . Journal of Universal Computer Science 23 , 1 (jan 2017), 63\u201388. Henning Basold, Herman Geuvers, and Niels van der Weide. 2017. Higher Inductive Types in Programming. Journal of Universal Computer Science 23, 1 (jan 2017), 63\u201388.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"e_1_3_2_2_11_1","volume-title":"19th International Conference on Types for Proofs and Programs, TYPES 2013","author":"Bezem Marc","year":"2013","unstructured":"Marc Bezem , Thierry Coquand , and Simon Huber . 2013 . A Model of Type Theory in Cubical Sets . In 19th International Conference on Types for Proofs and Programs, TYPES 2013 , April 22-26, 2013, Toulouse, France. 107\u2013128. Marc Bezem, Thierry Coquand, and Simon Huber. 2013. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs, TYPES 2013, April 22-26, 2013, Toulouse, France. 107\u2013128."},{"key":"e_1_3_2_2_12_1","volume-title":"On Streams that are Finitely Red. Logical Methods in Computer Science 8, 4","author":"Bezem Marc","year":"2012","unstructured":"Marc Bezem , Keiko Nakata , and Tarmo Uustalu . 2012. On Streams that are Finitely Red. Logical Methods in Computer Science 8, 4 ( 2012 ). Marc Bezem, Keiko Nakata, and Tarmo Uustalu. 2012. On Streams that are Finitely Red. Logical Methods in Computer Science 8, 4 (2012)."},{"key":"e_1_3_2_2_13_1","volume-title":"Constructive Analysis","author":"Bishop Errett","unstructured":"Errett Bishop and Douglas Bridges . 1985. Constructive Analysis . Springer Berlin Heidelberg . Errett Bishop and Douglas Bridges. 1985. Constructive Analysis. Springer Berlin Heidelberg."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275881"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628139"},{"key":"e_1_3_2_2_16_1","volume-title":"Cubical Type Theory: a Constructive Interpretation of the Univalence Axiom. CoRR abs\/1611.02108","author":"Cohen Cyril","year":"2016","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 2016. Cubical Type Theory: a Constructive Interpretation of the Univalence Axiom. CoRR abs\/1611.02108 ( 2016 ). http:\/\/arxiv.org\/abs\/1611. 02108 Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2016. Cubical Type Theory: a Constructive Interpretation of the Univalence Axiom. CoRR abs\/1611.02108 (2016). http:\/\/arxiv.org\/abs\/1611. 02108"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854076"},{"key":"e_1_3_2_2_18_1","volume-title":"Proceedings of MFPS","author":"Dybjer Peter","year":"2017","unstructured":"Peter Dybjer and Hugo Moeneclaey . 2017 . Finitary Higher Inductive Types in the Groupoid Model . In Proceedings of MFPS 2017, Electronic Notes in Theoretical Computer Science , Vol. to appear. Elsevier. Peter Dybjer and Hugo Moeneclaey. 2017. Finitary Higher Inductive Types in the Groupoid Model. In Proceedings of MFPS 2017, Electronic Notes in Theoretical Computer Science, Vol. to appear. Elsevier."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2808098.2808102"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.207.4"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018614"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316071"},{"key":"e_1_3_2_2_23_1","volume-title":"The Groupoid Interpretation of Type Theory. Twenty-five years of constructive type theory (Venice","author":"Hofmann Martin","year":"1995","unstructured":"Martin Hofmann and Thomas Streicher . 1998. The Groupoid Interpretation of Type Theory. Twenty-five years of constructive type theory (Venice , 1995 ) 36 (1998), 83\u2013111. Martin Hofmann and Thomas Streicher. 1998. The Groupoid Interpretation of Type Theory. Twenty-five years of constructive type theory (Venice, 1995) 36 (1998), 83\u2013111."},{"key":"e_1_3_2_2_24_1","volume-title":"The Seifert-van Kampen Theorem in Homotopy Type Theory. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016","author":"Michael Shulman Kuen-Bang","year":"2016","unstructured":"Kuen-Bang Hou (Favonia) and Michael Shulman . 2016 . The Seifert-van Kampen Theorem in Homotopy Type Theory. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 , August 29 - September 1, 2016, Marseille, France. 22:1\u201322:16. Kuen-Bang Hou (Favonia) and Michael Shulman. 2016. The Seifert-van Kampen Theorem in Homotopy Type Theory. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France. 22:1\u201322:16."},{"key":"e_1_3_2_2_25_1","volume-title":"Sketches of an Elephant: a Topos Theory Compendium","author":"Johnstone Peter T","unstructured":"Peter T Johnstone . 2002. Sketches of an Elephant: a Topos Theory Compendium . Vol. 2 . Oxford University Press . Peter T Johnstone. 2002. Sketches of an Elephant: a Topos Theory Compendium. Vol. 2. Oxford University Press."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933586"},{"key":"e_1_3_2_2_27_1","volume-title":"Type Classes for Efficient Exact Real Arithmetic in Coq. Logical Methods in Computer Science 9, 1","author":"Krebbers Robbert","year":"2011","unstructured":"Robbert Krebbers and Bas Spitters . 2011. Type Classes for Efficient Exact Real Arithmetic in Coq. Logical Methods in Computer Science 9, 1 ( 2011 ). Robbert Krebbers and Bas Spitters. 2011. Type Classes for Efficient Exact Real Arithmetic in Coq. Logical Methods in Computer Science 9, 1 (2011)."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693571"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm-1-1-129-131"},{"key":"e_1_3_2_2_30_1","first-page":"87","article-title":"First-Class Containers in Coq","volume":"9","author":"Lescuyer St\u00e9phane","year":"2011","unstructured":"St\u00e9phane Lescuyer . 2011 . First-Class Containers in Coq . Stud. Inform. Univ. 9 , 1 (2011), 87 \u2013 127 . St\u00e9phane Lescuyer. 2011. First-Class Containers in Coq. Stud. Inform. Univ. 9, 1 (2011), 87\u2013127.","journal-title":"Stud. Inform. Univ."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_1"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603153"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103697"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_3_2_2_36_1","volume-title":"Semantics of Higher Inductive Types. arXiv preprint arXiv:1705.07088","author":"LeFanu Lumsdaine Peter","year":"2017","unstructured":"Peter LeFanu Lumsdaine and Mike Shulman . 2017. Semantics of Higher Inductive Types. arXiv preprint arXiv:1705.07088 ( 2017 ). Peter LeFanu Lumsdaine and Mike Shulman. 2017. Semantics of Higher Inductive Types. arXiv preprint arXiv:1705.07088 (2017)."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25318-8_26"},{"key":"e_1_3_2_2_38_1","volume-title":"Investigating Streamless Sets. In 20th International Conference on Types for Proofs and Programs, TYPES 2014","author":"Parmann Erik","year":"2014","unstructured":"Erik Parmann . 2014 . Investigating Streamless Sets. In 20th International Conference on Types for Proofs and Programs, TYPES 2014 , May 12-15, 2014, Paris, France. 187\u2013201. Erik Parmann. 2014. Investigating Streamless Sets. In 20th International Conference on Types for Proofs and Programs, TYPES 2014, May 12-15, 2014, Paris, France. 187\u2013201."},{"key":"e_1_3_2_2_39_1","volume-title":"Some Varieties of Constructive Finiteness. In 19th Int. Conf. on Types for Proofs and Programs. 67\u201369","author":"Parmann Erik","year":"2014","unstructured":"Erik Parmann . 2014 . Some Varieties of Constructive Finiteness. In 19th Int. Conf. on Types for Proofs and Programs. 67\u201369 . Erik Parmann. 2014. Some Varieties of Constructive Finiteness. In 19th Int. Conf. on Types for Proofs and Programs. 67\u201369."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000553"},{"key":"e_1_3_2_2_41_1","volume-title":"Hereditarily Finite Sets in Constructive Type Theory","author":"Smolka Gert","unstructured":"Gert Smolka and Kathrin Stark . 2016. Hereditarily Finite Sets in Constructive Type Theory . Springer International Publishing , Cham , 374\u2013 390. Gert Smolka and Kathrin Stark. 2016. Hereditarily Finite Sets in Constructive Type Theory. Springer International Publishing, Cham, 374\u2013 390."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676983"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_2_44_1","unstructured":"Arnaud Spiwack and Thierry Coquand. 2010. Constructively Finite? In Contribuciones cient\u00edficas en honor de Mirian Andr\u00e9s G\u00f3mez Laureano Lamb\u00e1n Pardo Ana Romero Ib\u00e1\u00f1ez and Julio Rubio Garc\u00eda (Eds.). Universidad de La Rioja 217\u2013230. https:\/\/hal.inria.fr\/inria-00503917  Arnaud Spiwack and Thierry Coquand. 2010. Constructively Finite? In Contribuciones cient\u00edficas en honor de Mirian Andr\u00e9s G\u00f3mez Laureano Lamb\u00e1n Pardo Ana Romero Ib\u00e1\u00f1ez and Julio Rubio Garc\u00eda (Eds.). Universidad de La Rioja 217\u2013230. https:\/\/hal.inria.fr\/inria-00503917"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_3_2_2_46_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory. org\/book","author":"Foundations Program The Univalent","unstructured":"The Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory. org\/book , Institute for Advanced Study . The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory. org\/book, Institute for Advanced Study."},{"key":"e_1_3_2_2_47_1","volume-title":"The Delay Monad and Restriction Categories","author":"Uustalu Tarmo","unstructured":"Tarmo Uustalu and Niccol\u00f2 Veltri . 2017. The Delay Monad and Restriction Categories . Springer International Publishing , Cham , 32\u201350. Tarmo Uustalu and Niccol\u00f2 Veltri. 2017. The Delay Monad and Restriction Categories. Springer International Publishing, Cham, 32\u201350."},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000041"},{"key":"e_1_3_2_2_49_1","volume-title":"Homotopy Type Theory in Lean. In International Conference on Interactive Theorem Proving. Springer, 479\u2013495","author":"van Doorn Floris","year":"2017","unstructured":"Floris van Doorn , Jakob von Raumer , and Ulrik Buchholtz . 2017 . Homotopy Type Theory in Lean. In International Conference on Interactive Theorem Proving. Springer, 479\u2013495 . Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz. 2017. Homotopy Type Theory in Lean. In International Conference on Interactive Theorem Proving. Springer, 479\u2013495."},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1112\/jlms\/s2-47.2.193"},{"key":"e_1_3_2_2_51_1","unstructured":"Vladimir Voevodsky Benedikt Ahrens Daniel Grayson etal 2017. UniMath: Univalent Mathematics. Available at https:\/\/github.com\/ UniMath .  Vladimir Voevodsky Benedikt Ahrens Daniel Grayson et al. 2017. UniMath: Univalent Mathematics. Available at https:\/\/github.com\/ UniMath ."}],"event":{"name":"CPP '18: Certified Proofs and Programs","location":"Los Angeles CA USA","acronym":"CPP '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"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\/3167085","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167085","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:27Z","timestamp":1750212807000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167085"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":50,"alternative-id":["10.1145\/3167085","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167085","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"}}]}}