2026-08-04T20:49:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20339 2024-07-05T06:20:34Z ddc:004 open_access

Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics Kaposi, Ambrus Xie, Szumi Type theory universal algebra inductive types quotient inductive types higher-order abstract syntax logical framework Programming languages can be defined from the concrete to the abstract by abstract syntax trees, well-scoped syntax, well-typed (intrinsic) syntax, algebraic syntax (well-typed syntax quotiented by conversion). Another aspect is the representation of binding structure for which nominal approaches, De Bruijn indices/levels and higher order abstract syntax (HOAS) are available. In HOAS, binders are given by the function space of an internal language of presheaves. In this paper, we show how to combine the algebraic approach with the HOAS approach: following Uemura, we define languages as second-order generalised algebraic theories (SOGATs). Through a series of examples we show that non-substructural languages can be naturally defined as SOGATs. We give a formal definition of SOGAT signatures (using the syntax of a particular SOGAT) and define two translations from SOGAT signatures to GAT signatures (signatures for quotient inductive-inductive types), based on parallel and single substitutions, respectively. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ambrus Kaposi and Szumi Xie 2024 Is Part Of LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2024.10 urn:nbn:de:0030-drops-203396 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.10 eng https://creativecommons.org/licenses/by/4.0/legalcode