Theory Presentation Combinators

DOI10.1007/978-3-642-31374-5_14zbMath1360.68802arXiv1204.0053OpenAlexW1778672286WikidataQ60712726 ScholiaQ60712726MaRDI QIDQ2907324

Jacques Carette, Russell O'Connor

Publication date: 7 September 2012

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1204.0053

Mathematics Subject Classification ID

Knowledge representation (68T30) Fibered categories (18D30)

Related Items (4)

Automatically proving equivalence by type-safe reflection ⋮ Theory Presentation Combinators ⋮ Structure-preserving diagram operators ⋮ Realms: A Structure for Consolidating Knowledge about Mathematical Theories

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A scalable module system
• Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
• Generalized algebraic theories and contextual categories
• Categorical logic and type theory
• Constructing specification morphisms
• Detecting equivalence of modular specifications with categorical diagrams
• Theory Presentation Combinators
• Type classes for mathematics in type theory
• Packaging Mathematical Structures
• Some Considerations on the Usability of Interactive Provers
• On Duplication in Mathematical Repositories
• High-Level Theories

This page was built for publication: Theory Presentation Combinators