Diagram Combinators in MMT
Rabe F, Sharoda Y (2019)
Publication Type: Conference contribution
Publication year: 2019
Journal
Publisher: Springer Verlag
Book Volume: 11617 LNAI
Pages Range: 211-226
Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Event location: Prague
ISBN: 9783030232498
DOI: 10.1007/978-3-030-23250-4_15
Abstract
Formal libraries, especially large ones, usually employ modularity to build and maintain large theories efficiently. Although the techniques used to achieve modularity vary between systems, most of them can be understood as operations in the category of theories and theory morphisms. This yields a representation of libraries as diagrams in this category, with all theory-forming operations extending the diagram. However, as libraries grow even bigger, it is starting to become important to build these diagrams modularly as well, i.e., we need languages and tools that support computing entire diagrams at once. A simple example would be to systematically apply the same operation to all theories in a diagram and return both the new diagram and the morphisms that relate the old one to the new one. In this work, we introduce such diagram combinators as an extension to the MMT language and tool. We provide many important combinators, and our extension allows library developers to define arbitrary new ones. We evaluate our framework by building a library of algebraic theories in an extremely compact way.
Authors with CRIS profile
Involved external institutions
Canada (CA)How to cite
APA:
Rabe, F., & Sharoda, Y. (2019). Diagram Combinators in MMT. In Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 211-226). Prague, CZ: Springer Verlag.
MLA:
Rabe, Florian, and Yasmine Sharoda. "Diagram Combinators in MMT." Proceedings of the 12th International Conference on Intelligent Computer Mathematics, CICM 2019, Prague Ed. Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk, Springer Verlag, 2019. 211-226.
BibTeX: Download