Initiality for Typed Syntax and Semantics

TL;DR

This thesis develops an algebraic, initiality-based framework for simply-typed languages, enabling type-safe translations and formal verification of syntax and semantics using category theory and Coq.

Contribution

It introduces a universal property-based characterization of typed syntax and semantics via initial objects, facilitating safe translations and formal proofs in Coq.

Findings

Initiality provides a universal iteration principle for syntax translations.

Translations are inherently type-safe and reduction-faithful.

Formalization in Coq yields certified syntax and reduction machinery.

Abstract

In this thesis we give an algebraic characterization of the syntax and semantics of simply-typed languages. More precisely, we characterize simply-typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category. We specify a language by a 2-signature ({\Sigma}, A), that is, a signature on two levels: the syntactic level {\Sigma} specifies the sorts and terms of the language, and associates a sort to each term. The semantic level A specifies, through inequations, reduction rules on the terms of the language. To any given 2-signature ({\Sigma}, A) we associate a category of "models" of ({\Sigma}, A). We prove that this category has an initial object, which integrates the terms freely generated by {\Sigma} and the reduction relation - on those terms - generated by A. We call this object the programming language generated by ({\Sigma}, A). Initiality provides an iteration principle which allows to specify translations on the syntax, possibly to a language over different sorts. Furthermore, translations specified via the iteration principle are by construction type-safe and faithful with respect to reduction. To illustrate our results, we consider two examples extensively: firstly, we specify a double negation translation from classical to intuitionistic propositional logic via the category-theoretic iteration principle. Secondly, we specify a translation from PCF to the untyped lambda calculus which is faithful with respect to reduction in the source and target languages. In a second part, we formalize some of our initiality theorems in the proof assistant Coq. The implementation yields a machinery which, when given a 2-signature, returns an implementation of its associated abstract syntax together with certified substitution operation, iteration operator and a reduction relation generated by the specified reduction rules.