Categorical models of second-order abstract syntax

Mathematics and computer science increasingly rely on proof assistants to verify reasoning and ensure program correctness. Yet a persistent obstacle in the formalisation of programming languages and calculi is the treatment of variables and the associated operations of α-renaming and capture-avoiding substitution. Despite many proposed approaches, none match the flexibility and clarity of informal reasoning on paper. As a result, formalising languages in proof assistants often demands navigating a cumbersome layer of syntactic metatheory before any real benefits of mechanisation can be realised. In parallel, mathematical frameworks offer powerful, reusable tools for working with syntax – such as type-preserving simultaneous substitution and compositional semantics via initial algebras. However, their practical impact on formal verification has been limited, due to their categorical sophistication and the challenges of encoding them in dependently-typed settings. This thesis bridges this gap by formally relating the method of intrinsically typed encodings to the presheaf approach for languages with binding. We introduce the familial model of second-order abstract syntax as a categorical foundation for intrinsic typing, and show its equivalence to the presheaf model both syntactically and semantically. This places many ad hoc practices on solid mathematical footing, opening up principled paths for abstraction and extension. Along the way, we develop general tools for weakened monoidal structures and functorial models of syntax, framed by adjoint modalities – laying the groundwork for scalable and mechanised reasoning about syntax.

Name dc:type.qualificationname

Doctor of Philosophy (PhD)

Level dc:type.qualificationlevel

Doctoral

Grantor dc:publisher.institution

University of Cambridge

Year dc:date.issued

2025

Author dc:creator

• Szamozvancev, Dmitrij

Advisor dc:contributor.advisor

• Fiore, Marcelo

• category theory
• abstract syntax
• programming language theory
• computer formalisation

Licence

• https://www.repository.cam.ac.uk/bitstreams/c7824775-ccbe-4796-9d3b-8cbda4f05ab5/download
• http://purl.org/NET/rdflicense/allrightsreserved

Language dc:language

eng

Author Identifier

0000-0002-5436-6302
0000-0001-8558-3492

OAI identifier oai:identifier

oai:www.repository.cam.ac.uk:1810/399246