2 Search Results for "Stump, Aaron"


Document
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-dev.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}
}
Document
Type Preservation as a Confluence Problem

Authors: Aaron Stump, Garrin Kimmell, and Roba El Haj Omar

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)


Abstract
This paper begins with recent work by Kuan, MacQueen, and Findler, which shows how standard type systems, such as the simply typed lambda calculus, can be viewed as abstract reduction systems operating on terms. The central idea is to think of the process of typing a term as the computation of an abstract value for that term. The standard metatheoretic property of type preservation can then be seen as a confluence problem involving the concrete and abstract operational semantics, viewed as abstract reduction systems (ARSs). In this paper, we build on the work of Kuan et al. by showing show how modern ARS theory, in particular the theory of decreasing diagrams, can be used to establish type preservation via confluence. We illustrate this idea through several examples of solving such problems using decreasing diagrams. We also consider how automated tools for analysis of term-rewriting systems can be applied in testing type

Cite as

Aaron Stump, Garrin Kimmell, and Roba El Haj Omar. Type Preservation as a Confluence Problem. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 345-360, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{stump_et_al:LIPIcs.RTA.2011.345,
  author =	{Stump, Aaron and Kimmell, Garrin and El Haj Omar, Roba},
  title =	{{Type Preservation as a Confluence Problem}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{345--360},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.345},
  URN =		{urn:nbn:de:0030-drops-31343},
  doi =		{10.4230/LIPIcs.RTA.2011.345},
  annote =	{Keywords: Term rewriting, Type Safety, Confluence}
}
  • Refine by Author
  • 2 Stump, Aaron
  • 1 El Haj Omar, Roba
  • 1 Jenkins, Christa
  • 1 Kimmell, Garrin
  • 1 Marmaduke, Andrew

  • Refine by Classification
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Cedille
  • 1 Confluence
  • 1 Mendler algebra
  • 1 Term rewriting
  • 1 Type Safety
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2011
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail