Syntax and Semantics of Abstract Binding Trees

TL;DR

This paper introduces multi-sorted nominal abstract binding trees with formal syntax and semantics, supporting complex language features, and implements their categorical semantics in Agda, advancing proof assistant foundations.

Contribution

It extends second order universal algebra to multi-sorted nominal abts with formal semantics in Constructive Type Theory, supporting languages with generative phenomena.

Findings

Developed syntax and semantics for multi-sorted nominal abts

Formalized categorical semantics in Agda

Laid groundwork for the next version of the JonPRL proof assistant

Abstract

The contribution of this paper is the development of the syntax and semantics of multi-sorted nominal abstract binding trees (abts), an extension of second order universal algebra to support symbol-indexed families of operators. Nominal abts are essential for correctly treating the syntax of languages with generative phenomena, including exceptions and mutable state. Additionally we have developed the categorical semantics for abstract binding trees formally in Constructive Type Theory using the Agda proof assistant. Multi-sorted nominal abts also form the syntactic basis for the upcoming version of the JonPRL proof assistant, an implementation of an extensional constructive type theory in the Nuprl tradition.