Implementing a Category-Theoretic Framework for Typed Abstract Syntax
| Autor: | Benedikt Ahrens, Ralph Matthes, Anders Mörtberg |
|---|---|
| Přispěvatelé: | University of Birmingham [Birmingham], Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, University of Gothenburg (GU) |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
FOS: Computer and information sciences
formalization [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Computer Science - Programming Languages monad [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering Mathematics - Category Theory computer-checked proof 0102 computer and information sciences 02 engineering and technology 01 natural sciences 010201 computation theory & mathematics Mathematics::Category Theory typed abstract syntax 0202 electrical engineering electronic engineering information engineering FOS: Mathematics Category Theory (math.CT) signature [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT] Programming Languages (cs.PL) |
| Zdroj: | CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP 2022 (à paraître) Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’22) 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022) 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022), Jan 2022, Philadelphia, PA, United States. ⟨10.1145/3497775.3503678⟩ |
| DOI: | 10.1145/3497775.3503678⟩ |
| Popis: | Accepted to CPP 2022; International audience; In previous work (“From signatures to monads in UniMath”), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof assistant. In the present work, we describe what was necessary to generalize that work to account for simply-typed languages. First, some definitions had to be generalized to account for the natural appearance of non-endofunctors in the simply typed case. As it turns out, in many cases our mechanized results carried over to the generalized definitions without any code change. Second, an existing mechanized library on ω-cocontinuous functors had to be extended by constructions and theorems necessary for constructing multi-sorted syntax. Third, the theoretical framework for the semantical signatures had to be generalized from a monoidal to a bi-categorical setting, again to account for non-endofunctors arising in the typed case. This uses actions of endofunctors on functors with given source, and the corresponding notion of strong functors between actions, all formalized in UniMath using a recently developed library of bicategory theory. We explain what needed to be done to plug all of these ingredients together, modularly. The main result of our work is a general construction that, when fed with a signature for a simply-typed language, returns an implementation of that language together with suitable boilerplate code, in particular, a certified monadic substitution operation. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|