文章基本信息

标题：Data Types as Quotients of Polynomial Functors
本地全文：下载
作者：Jeremy Avigad ; Mario Carneiro ; Simon Hudon 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：141
页码：1-19
DOI：10.4230/LIPIcs.ITP.2019.6
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：data types; polynomial functors; inductive types; coinductive types