License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.14
URN: urn:nbn:de:0030-drops-183891
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18389/
Dunn, Lawrence ;
Tannen, Val ;
Zdancewic, Steve
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure
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.
BibTeX - Entry
@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/opus/volltexte/2023/18389},
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}
}
