License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.6
URN: urn:nbn:de:0030-drops-110612
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11061/
Go to the corresponding LIPIcs Volume Portal

Avigad, Jeremy ; Carneiro, Mario ; Hudon, Simon

Data Types as Quotients of Polynomial Functors

pdf-format:
LIPIcs-ITP-2019-6.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{avigad_et_al:LIPIcs:2019:11061,
  author =	{Jeremy Avigad and Mario Carneiro and Simon Hudon},
  title =	{{Data Types as Quotients of Polynomial Functors}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11061},
  URN =		{urn:nbn:de:0030-drops-110612},
  doi =		{10.4230/LIPIcs.ITP.2019.6},
  annote =	{Keywords: data types, polynomial functors, inductive types, coinductive types}
}

Keywords: data types, polynomial functors, inductive types, coinductive types
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: Lean formalizations are online at www.github.com/avigad/qpf.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI