DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2023.14

Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure

Authors: Lawrence Dunn, Val Tannen, and Steve Zdancewic

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract

Verifying the metatheory of a formal system in Coq involves a lot of tedious "infrastructural" reasoning about variable binders. We present Tealeaves, a generic framework for first-order representations of variable binding that can be used to develop this sort of infrastructure once and for all. Given a particular strategy for representing binders concretely, such as locally nameless or de Bruijn indices, Tealeaves allows developers to implement modules of generic infrastructure called backends that end users can simply instantiate to their own syntax. Our framework rests on a novel abstraction of first-order abstract syntax called a decorated traversable monad (DTM) whose equational theory provides reasoning principles that replace tedious induction on terms. To evaluate Tealeaves, we have implemented a multisorted locally nameless backend providing generic versions of the lemmas generated by LNgen. We discuss case studies where we instantiate this generic infrastructure to simply-typed and polymorphic lambda calculi, comparing our approach to other utilities.

Cite as

Lawrence Dunn, Val Tannen, and Steve Zdancewic. Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dunn_et_al:LIPIcs.ITP.2023.14,
  author =	{Dunn, Lawrence and Tannen, Val and Zdancewic, Steve},
  title =	{{Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.14},
  URN =		{urn:nbn:de:0030-drops-183891},
  doi =		{10.4230/LIPIcs.ITP.2023.14},
  annote =	{Keywords: Coq, category theory, formal metatheory, raw syntax, locally nameless}
}

Search Results

Documents authored by Dunn, Lawrence

Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure

Abstract

Cite as

Thanks for your feedback!

Could not send message