2026-08-04T19:03:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14268 2024-03-06T10:53:18Z ddc:004 open_access

Abstract Clones for Abstract Syntax Arkor, Nathanael McDermott, Dylan simple type theories abstract clones second-order abstract syntax substitution variable binding presentations free algebras induction logical relations We give a formal treatment of simple type theories, such as the simply-typed λ-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed λ-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as β- and η-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nathanael Arkor and Dylan McDermott 2021 Is Part Of LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2021.30 urn:nbn:de:0030-drops-142686 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.30 eng https://creativecommons.org/licenses/by/4.0/legalcode