This program is tentative and subject to change.

Sat 22 Jan 2022 11:00 - 11:20 at Salon I - Contributed Talks (Morning) Chair(s): Benjamin C. Pierce

Verifying the properties of formal frameworks such as lambda calculi involves a lot of laborious reasoning about syntax, which it is therefore desirable to automate. We contribute to this goal by identifying several category-theoretic notions that together constitute an abstract definition of syntax with binders. Using these abstractions, which we have implemented in a Coq library called Tealeaves, we show that much purely syntactical reasoning can be formalized in Coq just once, generically over syntax, and later specialized to any particular syntax. This is because Tealeaves supports proving theorems that are parametric over a choice of decorated traversable monad (DTM), representing a concrete syntax. This allows us to formalize syntactical reasoning in Tealeaves backends, which are Coq libraries that use Tealeaves to define the operations of and prove theorems about one of the standard techniques for representing bound variables (e.g. de Bruijn indices, locally nameless, etc.). Since each backend reasons generically over DTMs, the definitions and proofs it provides can be applied to any syntax as soon as we formalize it as a decorated traversable monad. This reduces the problem of synthesizing syntactical reasoning to generating instances of these monads from a user-provided syntax, a clear and conceptually simple problem.

Our talk will discuss these novel abstractions and show how Tealeaves is used by a backend to reason about syntax generically, focusing on a completed case study: proving progress and preservation theorems for System F using a locally nameless backend that is generic over a choice of many-sorted syntax.

Abstract (coqpl22-final25.pdf)360KiB

This program is tentative and subject to change.

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 12:00
Contributed Talks (Morning)CoqPL at Salon I
Chair(s): Benjamin C. Pierce University of Pennsylvania
10:20
20m
Talk
A Visual Ltac Debugger in CoqIDERemote
CoqPL
S: Jim Fehrle None
File Attached
10:40
20m
Talk
Scrap your boilerplate definitions in 10 lines of Ltac!InPerson
CoqPL
S: Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
File Attached
11:00
20m
Talk
Tealeaves: Categorical structures for syntaxInPerson
CoqPL
S: Lawrence Dunn University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Val Tannen University of Pennsylvania, USA
File Attached
11:20
20m
Talk
Towards a Formalization of Nominal Sets in CoqRemote
CoqPL
S: Fabrício S. Paranhos Universidade Federal de Goiás, Daniel Ventura Universidade Federal de Goiás
File Attached
11:40
20m
Talk
A Case for Lightweight Interfaces in CoqInPerson
CoqPL
David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock Systems
File Attached
Hide past events