Theory Presentation Combinators
arXiv:1204.0053 · doi:10.1007/978-3-642-31374-5_14
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.
Extended version of paper to appear in proceedings of CICM 2012