{"id":{"repo_id":"cambridge","oai_identifier":"oai:www.repository.cam.ac.uk:1810/399246"},"canonical_url":"https://search.dev.ndltd.org/etd/cambridge/oai:www.repository.cam.ac.uk:1810/399246","repository":{"repo_id":"cambridge","name":"Cambridge University","base_url":"https://api.repository.cam.ac.uk/server/oai/request"},"display":{"title":"Categorical models of second-order abstract syntax","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Szamozvancev, Dmitrij"],"institution":"University of Cambridge","degree_name":"Doctor of Philosophy (PhD)","degree_level":"Doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Fiore, Marcelo"],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025-05-27","date_published":"2025-05-27","updated_at":"2026-07-22T22:24:31Z","subjects":["category theory","abstract syntax","programming language theory","computer formalisation"],"languages":["eng"],"rights":[],"rights_urls":["https://www.repository.cam.ac.uk/bitstreams/c7824775-ccbe-4796-9d3b-8cbda4f05ab5/download","http://purl.org/NET/rdflicense/allrightsreserved"],"identifier_entries":[{"key":"dc:creator.authoridentifier","label":"Author Identifier","values":["0000000254366302","0000000185583492"],"render_values":[{"text":"0000-0002-5436-6302","href":"https://orcid.org/0000-0002-5436-6302","code":true},{"text":"0000-0001-8558-3492","href":"https://orcid.org/0000-0001-8558-3492","code":true}]}]},"links":{"outbound_url":"https://doi.org/10.17863/CAM.127851","outbound_label":"DOI","outbound_source":"dc:identifier.doi"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Fiore, Marcelo"]},{"key":"dc:creator","label":"Author","values":["Szamozvancev, Dmitrij"]},{"key":"dc:creator.authoridentifier","label":"Author Identifier","values":["0000000254366302","0000000185583492"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.issued","label":"Date","values":["2025-05-27"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["University of Cambridge"]},{"key":"dc:relation.isreferencedby.uri","label":"Dc Relation Isreferencedby URI","values":["https://www.repository.cam.ac.uk/handle/1810/399246"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["Doctoral"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["Doctor of Philosophy (PhD)"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["category theory","abstract syntax","programming language theory","computer formalisation"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["https://www.repository.cam.ac.uk/bitstreams/c7824775-ccbe-4796-9d3b-8cbda4f05ab5/download","http://purl.org/NET/rdflicense/allrightsreserved"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.doi","label":"DOI","values":["https://doi.org/10.17863/CAM.127851"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://www.repository.cam.ac.uk/bitstreams/63913a42-4d88-44ac-8746-3f5478dbadb4/download"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format.checksum.md5","label":"Dc Format Checksum Md5","values":["08019d8ea951036c6e0edfa6a5b78911","87eda9de84448d1f82354d60eee3eb5f"]},{"key":"dc:title","label":"Title","values":["Categorical models of second-order abstract syntax"]}]}],"canonical_facts":{"dc:contributor.advisor":["Fiore, Marcelo"],"dc:creator":["Szamozvancev, Dmitrij"],"dc:creator.authoridentifier":["0000000254366302","0000000185583492"],"dc:date.issued":["2025-05-27"],"dc:description.abstract":["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."],"dc:format.checksum.md5":["08019d8ea951036c6e0edfa6a5b78911","87eda9de84448d1f82354d60eee3eb5f"],"dc:identifier.doi":["https://doi.org/10.17863/CAM.127851"],"dc:identifier.uri":["https://www.repository.cam.ac.uk/bitstreams/63913a42-4d88-44ac-8746-3f5478dbadb4/download"],"dc:language":["eng"],"dc:publisher.institution":["University of Cambridge"],"dc:relation.isreferencedby.uri":["https://www.repository.cam.ac.uk/handle/1810/399246"],"dc:rights":["https://www.repository.cam.ac.uk/bitstreams/c7824775-ccbe-4796-9d3b-8cbda4f05ab5/download","http://purl.org/NET/rdflicense/allrightsreserved"],"dc:subject":["category theory","abstract syntax","programming language theory","computer formalisation"],"dc:title":["Categorical models of second-order abstract syntax"],"dc:type":["Thesis"],"dc:type.qualificationlevel":["Doctoral"],"dc:type.qualificationname":["Doctor of Philosophy (PhD)"]},"updated_at":"2026-07-22T22:24:31Z"}