Incoherent coherences

TL;DR

This paper introduces a generic framework for well-typed syntaxes that reduces boilerplate code and proofs, inspired by algebraic approaches, to streamline the development of formal systems.

Contribution

It presents a novel signature-axiom framework that abstracts boilerplate code and proofs in defining and working with well-typed syntaxes.

Findings

Framework effectively reduces boilerplate in syntax definitions

Generalizes common proofs in syntax manipulation

Provides a structured algebraic approach to syntax

Abstract

This article explores a generic framework of well-typed and well-scoped syntaxes, with a signature-axiom approach resembling traditional abstract algebra. The boilerplate code needed in defining operations on syntaxes is identified and abstracted away. Some of the frequent boilerplate proofs are also generalized.