Tealeaves

Tealeaves is a Coq framework for proving theorems about syntax abstractly, i.e. independently of a concrete grammar. This independence makes syntactical theory reusable between developments, and is achieved by separating a choice of grammar from a choice of variable representation. Our central abstraction is a "structured" kind of monad that we call decorated traversable, which is an abstraction of abstract syntax trees. Tealeaves "core" is a Coq implementation of the equational theory of such monads, as well as higher-level principles built on top of this theory.

How to build Tealeaves

System requirements:

• make (see GNU Make)
• An installation of Coq >= 8.13 (see the Coq downloads page).

Compilation instructions:

• Run make in the top-level directory
• Run make clean to remove all build artifacts (including compiled files) and start over

We have tested with Coq 8.13, but other versions may work too. We observe a compilation time of approximately 4-5 minutes on a typical desktop computer. On multicore systems you may want to use the -j flag to use several build threads. We have sometimes observed that -j leads to cryptic build errors. The solution to these is simply to re-run the build command again.

Tealeaves is built with the coq_makefile, which is distributed with Coq itself. This utility generates a customized Makefile to build a Coq project. For simplicity, we provide a top-level Makefile which will call coq_makefile for you, and then recursively call make on the generated Makefile, so that you should not have to do anything except call make once in the top-level directory.

Generating the documentation

Pretty-printed HTML documentation is generated by default in the html/ directory.

Module organization

Typeclasses

Classes of "structured" functors (like monads, decorated monads, traversable functors, etc.) are found in under Tealeaves/Classes. The internal implementation of Tealeaves uses an algebraic rather than Kleisli-style implementation of our typeclasses, so that operations like bind are derived rather than taken as primitive. For example, decorated monads are defined here as monads equipped with a "decoration" operation. Their equivalent Kleisli presentation is derived here in the same file. A characterization of decorated functors as comodules of the reader/writer bimonad is found here.

The locally nameless backend

Our locally nameless backend library is formalized under the LN/ directory. The operations (opening, closing, local closure, etc) are defined here. Various lemmas about these operations, proved polymorphically over a decorated traversable monad T, are proved here.

Simply typed lambda calculus

Our formalization of STLC is under the STLC/ directory. A formalization of STLC's syntax as a DTM is found here. Basic metatheory such as a progress theorem are proved here.

Multisorted

Our multisorted classes live under Multisorted/. Our extension of the locally nameless backend lives under LN/Multisorted/. SystemF lives under SystemF.

Typeclasses hierarchy

Other notes

Axioms used in Tealeaves

Tealeaves currently uses two axioms commonly used in Coq formalizations, which have been proven (on paper) to be equi-consistent with Coq itself. They are the following.

• Propositional extensionality, which says that equivalent propositions (P <-> Q) are propositionally equal (P = Q)
• Functional extensionality, which is the statement forall x, f x = g x -> f = g.

There axioms are assumed here. They are a convenience to use Coq's rewriting features. In principle one can eliminate these at the cost of ``setoid hell'' (see this question on StackOverflow).