Owen Lynch ; Kris Brown ; James Fairbanks ; Evan Patterson - GATlab: Modeling and Programming with Generalized Algebraic Theories

entics:14666 - Electronic Notes in Theoretical Informatics and Computer Science, December 11, 2024, Volume 4 - Proceedings of MFPS XL - https://doi.org/10.46298/entics.14666
GATlab: Modeling and Programming with Generalized Algebraic TheoriesArticle

Authors: Owen Lynch ; Kris Brown ; James Fairbanks ; Evan Patterson

    Categories and categorical structures are increasingly recognized as useful abstractions for modeling in science and engineering. To uniformly implement category-theoretic mathematical models in software, we introduce GATlab, a domain-specific language for algebraic specification embedded in a technical programming language. GATlab is based on generalized algebraic theories (GATs), a logical system extending algebraic theories with dependent types so as to encompass category theory. Using GATlab, the programmer can specify generalized algebraic theories and their models, including both free models, based on symbolic expressions, and computational models, defined by arbitrary code in the host language. Moreover, the programmer can define maps between theories and use them to declaratively migrate models of one theory to models of another. In short, GATlab aims to provide a unified environment for both computer algebra and software interface design with generalized algebraic theories. In this paper, we describe the design, implementation, and applications of GATlab.


    Volume: Volume 4 - Proceedings of MFPS XL
    Published on: December 11, 2024
    Accepted on: November 7, 2024
    Submitted on: November 4, 2024
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages

    Consultation statistics

    This page has been seen 58 times.
    This article's PDF has been downloaded 39 times.