DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2021.9

Simulating Large Eliminations in Cedille

Authors: Christa Jenkins, Andrew Marmaduke, and Aaron Stump

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract

Large eliminations provide an expressive mechanism for arity- and type-generic programming. However, as large eliminations are closely tied to a type theory’s primitive notion of inductive type, this expressivity is not expected within polymorphic lambda calculi in which datatypes are encoded using impredicative quantification. We report progress on simulating large eliminations for datatype encodings in one such type theory, the calculus of dependent lambda eliminations (CDLE). Specifically, we show that the expected computation rules for large eliminations, expressed using a derived type of extensional equality of types, can be proven within CDLE. We present several case studies, demonstrating the adequacy of this simulation for a variety of generic programming tasks, and a generic formulation of the simulation allowing its use for a broad family of datatype encodings. All results have been mechanically checked by Cedille, an implementation of CDLE.

Cite as

Christa Jenkins, Andrew Marmaduke, and Aaron Stump. Simulating Large Eliminations in Cedille. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{jenkins_et_al:LIPIcs.TYPES.2021.9,
  author =	{Jenkins, Christa and Marmaduke, Andrew and Stump, Aaron},
  title =	{{Simulating Large Eliminations in Cedille}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{9:1--9:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.9},
  URN =		{urn:nbn:de:0030-drops-167784},
  doi =		{10.4230/LIPIcs.TYPES.2021.9},
  annote =	{Keywords: large eliminations, generic programming, impredicative encodings, Cedille, Mendler algebra}
}

Search Results

Documents authored by Marmaduke, Andrew

Simulating Large Eliminations in Cedille

Abstract

Cite as

Thanks for your feedback!

Could not send message