Theory presentation combinators
From MaRDI portal
Publication:2907324
DOI10.1007/978-3-642-31374-5_14zbMATH Open1360.68802arXiv1204.0053OpenAlexW1778672286WikidataQ60712726 ScholiaQ60712726MaRDI QIDQ2907324FDOQ2907324
Authors: Jacques Carette, Russell O'Connor 
Publication date: 7 September 2012
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1204.0053
Recommendations
- Diagram combinators in MMT
- Leveraging the information contained in theory presentations
- Building Structured Theories
- Some fundamental algebraic tools for the semantics of computation: II. Signed and abstract theories
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
Cites Work
- Categorical logic and type theory
- A scalable module system
- Generalized algebraic theories and contextual categories
- Title not available (Why is that?)
- Packaging Mathematical Structures
- On duplication in mathematical repositories
- Title not available (Why is that?)
- Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
- Some considerations on the usability of interactive provers
- Detecting equivalence of modular specifications with categorical diagrams
- Title not available (Why is that?)
- Constructing specification morphisms
- Type classes for mathematics in type theory
- High-Level Theories
- Theory presentation combinators
- Nonuniform coercions via unification hints
Cited In (5)
This page was built for publication: Theory presentation combinators
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2907324)
