GATlab：用广义代数理论进行建模与编程
GATlab: Modeling and Programming with Generalized Algebraic Theories
AI总结：
GATlab是一个基于广义代数理论的领域特定语言，用于统一实现范畴论模型，支持自由与计算模型及理论间迁移，旨在统一计算机代数与软件接口设计。
摘要：
范畴及范畴结构在科学与工程建模中日益被视为有用的抽象。为了在软件中统一实现范畴论数学模型，我们引入了GATlab，一种嵌入在技术编程语言中的领域特定语言，用于代数规范。GATlab基于广义代数理论（GATs），这是一种通过依赖类型扩展代数理论以涵盖范畴论的逻辑系统。使用GATlab，程序员可以指定广义代数理论及其模型，包括基于符号表达式的自由模型，以及由宿主语言中的任意代码定义的计算模型。此外，程序员可以定义理论之间的映射，并声明式地将一个理论的模型迁移到另一个理论的模型。简而言之，GATlab旨在为计算机代数和软件接口设计提供一个统一的环境，使用广义代数理论。在本文中，我们描述了GATlab的设计、实现和应用。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
