{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:12:15Z","timestamp":1750306335479,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,7,5]],"date-time":"2016-07-05T00:00:00Z","timestamp":1467676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["612.001.021"],"award-info":[{"award-number":["612.001.021"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,7,5]]},"DOI":"10.1145\/2933575.2934514","type":"proceedings-article","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T13:34:47Z","timestamp":1476452087000},"page":"327-336","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Type Theory based on Dependent Inductive and Coinductive Types"],"prefix":"10.1145","author":[{"given":"Henning","family":"Basold","sequence":"first","affiliation":[{"name":"Radboud University, CWI, Amsterdam"}]},{"given":"Herman","family":"Geuvers","sequence":"additional","affiliation":[{"name":"Radboud University, Technical University Eindhoven"}]}],"member":"320","published-online":{"date-parts":[[2016,7,5]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500591"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"e_1_3_2_1_3_1","volume-title":"Number 14 in Lecture Notes","author":"Aczel P.","year":"1988","unstructured":"P. Aczel . Non-well-founded Sets. Number 14 in Lecture Notes . Center for the Study of Language and Information, Stanford University , 1988 . P. Aczel. Non-well-founded Sets. Number 14 in Lecture Notes. Center for the Study of Language and Information, Stanford University, 1988."},{"key":"e_1_3_2_1_4_1","volume-title":"Programming Logic group","author":"Documentation Agda","year":"2015","unstructured":"Agda. Agda Documentation . Technical report , Programming Logic group , Chalmers and Gothenburg University , 2015 . URL http:\/\/wiki.portal.chalmers.se\/agda\/. Version 2.4.2.5. Agda. Agda Documentation. Technical report, Programming Logic group, Chalmers and Gothenburg University, 2015. URL http:\/\/wiki.portal.chalmers.se\/agda\/. Version 2.4.2.5."},{"key":"e_1_3_2_1_5_1","volume-title":"Apr.","author":"Ahrens B.","year":"2015","unstructured":"B. Ahrens , P. Capriotti , and R. Spadotti . Non-wellfounded trees in Homotopy Type Theory. ArXiv150402949 Cs Math , Apr. 2015 . B. Ahrens, P. Capriotti, and R. Spadotti. Non-wellfounded trees in Homotopy Type Theory. ArXiv150402949 Cs Math, Apr. 2015."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_1_7_1","series-title":"EPTCS","first-page":"3","volume-title":"Proceedings of FICS '15","author":"Basold H.","year":"2015","unstructured":"H. Basold . Dependent Inductive and Coinductive Types are Fibrational Dialgebras . In R. Matthes and M. Mio, editors, Proceedings of FICS '15 , volume 191 of EPTCS , pages 3 -- 17 . Open Publishing Association , Sept. 2015 . doi: 10.4204\/EPTCS.191.3. 10.4204\/EPTCS.191.3 H. Basold. Dependent Inductive and Coinductive Types are Fibrational Dialgebras. In R. Matthes and M. Mio, editors, Proceedings of FICS '15, volume 191 of EPTCS, pages 3--17. Open Publishing Association, Sept. 2015. doi: 10.4204\/EPTCS.191.3."},{"key":"e_1_3_2_1_8_1","unstructured":"H. Basold. Code Repository 2016. URL http:\/\/cs.ru.nl\/~hbasold\/code\/.  H. Basold. Code Repository 2016. URL http:\/\/cs.ru.nl\/~hbasold\/code\/."},{"key":"e_1_3_2_1_9_1","volume-title":"To Appear in JLC","author":"Basold H.","year":"2015","unstructured":"H. Basold and H. H. Hansen . Well-definedness and Observational Equivalence for Inductive-Coinductive Programs . To Appear in JLC , 2015 . H. Basold and H. H. Hansen. Well-definedness and Observational Equivalence for Inductive-Coinductive Programs. To Appear in JLC, 2015."},{"key":"e_1_3_2_1_10_1","series-title":"An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast\u00e9ran . Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science . An EATCS Series . Springer , 2004 . Y. Bertot and P. Cast\u00e9ran. Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_2"},{"volume-title":"Type Theoretic Interpretation of the Final Chain","year":"2016","key":"e_1_3_2_1_12_1","unstructured":"cLab. Type Theoretic Interpretation of the Final Chain , 2016 . URL https:\/\/coalg.org\/clab\/Type_Theoretic_Interpretation_of_the_Final_Chain. cLab. Type Theoretic Interpretation of the Final Chain, 2016. URL https:\/\/coalg.org\/clab\/Type_Theoretic_Interpretation_of_the_Final_Chain."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59048-1_4"},{"key":"e_1_3_2_1_14_1","volume-title":"LogiCal Project","author":"Team Coq Development","year":"2012","unstructured":"Coq Development Team . The Coq proof assistant reference manual. Technical report , LogiCal Project , 2012 . URL http:\/\/coq.inria.fr. Version 8.4. Coq Development Team. The Coq proof assistant reference manual. Technical report, LogiCal Project, 2012. URL http:\/\/coq.inria.fr. Version 8.4."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/646535.695848"},{"key":"e_1_3_2_1_16_1","first-page":"39","volume-title":"Selected Papers from the TYPES '94 Workshop","author":"Gim\u00e9nez E.","year":"1995","unstructured":"E. Gim\u00e9nez . Codifying Guarded Definitions with Recursive Schemes . In Selected Papers from the TYPES '94 Workshop , pages 39 -- 59 , London, UK , 1995 . Springer-Verlag . E. Gim\u00e9nez. Codifying Guarded Definitions with Recursive Schemes. In Selected Papers from the TYPES '94 Workshop, pages 39--59, London, UK, 1995. Springer-Verlag."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/648331.755419"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2036918.2036927"},{"key":"e_1_3_2_1_19_1","volume-title":"North Holland","author":"Jacobs B.","year":"1999","unstructured":"B. Jacobs . Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics . North Holland , Amsterdam , 1999 . B. Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999."},{"key":"e_1_3_2_1_20_1","volume-title":"Introduction to Higher-Order Categorical Logic","author":"Lambek J.","year":"1988","unstructured":"J. Lambek and P. J. Scott . Introduction to Higher-Order Categorical Logic . Cambridge University Press , Mar. 1988 . J. Lambek and P. J. Scott. Introduction to Higher-Order Categorical Logic. Cambridge University Press, Mar. 1988."},{"key":"e_1_3_2_1_21_1","first-page":"81","volume-title":"Martin-L\u00f6f. About Models for Intuitionistic Type Theories and the Notion of Definitional Equality. In 3rd Scandinavian Logic Symposium","author":"P.","year":"1975","unstructured":"P. Martin-L\u00f6f. About Models for Intuitionistic Type Theories and the Notion of Definitional Equality. In 3rd Scandinavian Logic Symposium , pages 81 -- 109 . North Holland and American Elsevier , 1975 . P. Martin-L\u00f6f. About Models for Intuitionistic Type Theories and the Notion of Definitional Equality. In 3rd Scandinavian Logic Symposium, pages 81--109. North Holland and American Elsevier, 1975."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_2_1_24_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"International Conference on Typed Lambda Calculi and Applications, TLCA, Proceedings","author":"Paulin-Mohring C.","year":"1993","unstructured":"C. Paulin-Mohring . Inductive definitions in the system Coq - rules and properties . In M. Bezem and J. F. Groote, editors, International Conference on Typed Lambda Calculi and Applications, TLCA, Proceedings , volume 664 of LNCS , pages 328 -- 345 . Springer , 1993 . C. Paulin-Mohring. Inductive definitions in the system Coq - rules and properties. In M. Bezem and J. F. Groote, editors, International Conference on Typed Lambda Calculi and Applications, TLCA, Proceedings, volume 664 of LNCS, pages 328--345. Springer, 1993."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.29"},{"key":"e_1_3_2_1_26_1","volume-title":"Institute for Advanced Study","author":"Foundations Program The Univalent","year":"2013","unstructured":"The Univalent Foundations Program . Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book , Institute for Advanced Study , 2013 . The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book, Institute for Advanced Study, 2013."},{"key":"e_1_3_2_1_27_1","volume-title":"North-Holland","author":"Troelstra A. S.","year":"1988","unstructured":"A. S. Troelstra and D. van Dalen . Constructivism in Mathematics: An Introduction . North-Holland , 1988 . A. S. Troelstra and D. van Dalen. Constructivism in Mathematics: An Introduction. North-Holland, 1988."},{"key":"e_1_3_2_1_28_1","volume-title":"Predicative topos theory and models for constructive set theory. Phd","author":"van den Berg B.","year":"2006","unstructured":"B. van den Berg . Predicative topos theory and models for constructive set theory. Phd , University of Utrecht , 2006 . B. van den Berg. Predicative topos theory and models for constructive set theory. Phd, University of Utrecht, 2006."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2006.12.001"},{"key":"e_1_3_2_1_30_1","volume-title":"Universit\u00e9 Paris VII","author":"Werner B.","year":"1994","unstructured":"B. Werner . Une th\u00e9orie des Constructions Inductives. Phd , Universit\u00e9 Paris VII , 1994 . B. Werner. Une th\u00e9orie des Constructions Inductives. Phd, Universit\u00e9 Paris VII, 1994."}],"event":{"name":"LICS '16: 31st Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"location":"New York NY USA","acronym":"LICS '16"},"container-title":["Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2933575.2934514","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2933575.2934514","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:54:53Z","timestamp":1750222493000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2933575.2934514"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,5]]},"references-count":29,"alternative-id":["10.1145\/2933575.2934514","10.1145\/2933575"],"URL":"https:\/\/doi.org\/10.1145\/2933575.2934514","relation":{},"subject":[],"published":{"date-parts":[[2016,7,5]]},"assertion":[{"value":"2016-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}