Theory presentation combinators

DOI10.1007/978-3-642-31374-5_14MaRDI QIDQ2907324zbMATH OpenOpenAlexWikidataFDO

Authors 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)

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

(9)

• Theory presentation combinators
• Structure-preserving diagram operators
• Diagram combinators in MMT
• Automatically proving equivalence by type-safe reflection
• GATlab: modeling and programming with generalized algebraic theories
• Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description)
• Global, regional, and local contexts
• Realms: a structure for consolidating knowledge about mathematical theories
• Rapid prototyping formal systems in MMT: 5 case studies

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)