2026-07-21T12:58:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11061 2024-03-06T10:47:16Z ddc:004 open_access

Data Types as Quotients of Polynomial Functors Avigad, Jeremy Carneiro, Mario Hudon, Simon data types polynomial functors inductive types coinductive types A broad class of data types, including arbitrary nestings of inductive types, coinductive types, and quotients, can be represented as quotients of polynomial functors. This provides perspicuous ways of constructing them and reasoning about them in an interactive theorem prover. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jeremy Avigad and Mario Carneiro and Simon Hudon 2019 Is Part Of LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2019.6 urn:nbn:de:0030-drops-110612 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.6 eng https://creativecommons.org/licenses/by/3.0/legalcode