Theory presentation combinators
From MaRDI portal
Publication:2907324
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.
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
- scientific article; zbMATH DE number 3714904 (Why is no real title available?)
- scientific article; zbMATH DE number 2085169 (Why is no real title available?)
- scientific article; zbMATH DE number 1390335 (Why is no real title available?)
- A scalable module system
- Categorical logic and type theory
- Constructing specification morphisms
- Detecting equivalence of modular specifications with categorical diagrams
- Generalized algebraic theories and contextual categories
- High-Level Theories
- Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
- Nonuniform coercions via unification hints
- On duplication in mathematical repositories
- Packaging Mathematical Structures
- Some considerations on the usability of interactive provers
- Theory presentation combinators
- Type classes for mathematics in type theory
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)
