Theory Presentation Combinators
Mathematical Software
2014-02-25 v2 Symbolic Computation
Category Theory
Abstract
We motivate and give semantics to theory presentation combinators as the foundational building blocks for a scalable library of theories. The key observation is that the category of contexts and fibered categories are the ideal theoretical tools for this purpose.
Cite
@article{arxiv.1204.0053,
title = {Theory Presentation Combinators},
author = {Jacques Carette and Russell O'Connor},
journal= {arXiv preprint arXiv:1204.0053},
year = {2014}
}
Comments
Extended version of paper to appear in proceedings of CICM 2012