A scalable module system
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1617292 (Why is no real title available?)
- scientific article; zbMATH DE number 986407 (Why is no real title available?)
- scientific article; zbMATH DE number 3819086 (Why is no real title available?)
- scientific article; zbMATH DE number 108434 (Why is no real title available?)
- scientific article; zbMATH DE number 3467028 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 3527483 (Why is no real title available?)
- scientific article; zbMATH DE number 1216133 (Why is no real title available?)
- scientific article; zbMATH DE number 1231537 (Why is no real title available?)
- scientific article; zbMATH DE number 2079832 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 3280051 (Why is no real title available?)
- scientific article; zbMATH DE number 3331288 (Why is no real title available?)
- A foundational view on integration problems
- A framework for defining logics
- A logical framework combining model and proof theory
- A proof theoretic interpretation of model theoretic hiding
- A query language for formal mathematical libraries
- A universal machine for biform theory graphs
- An Integrated Development Environment for Collections
- CASL reference manual. The complete documentation of the common algebraic specification language.
- Crafting a Proof Assistant
- Development graphs -- proof management for structured specifications
- Extending MKM formats at the statement level
- FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
- Formalising foundations of mathematics
- IMPS: An interactive mathematical proof system
- Institutions: abstract model theory for specification and programming
- Integrating Web Services into Active Mathematical Documents
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle. A generic theorem prover
- Notations for Living Mathematical Documents
- Nuprl's class theory and its applications
- On finite simple groups and their classification.
- OpenMath in SCIEnce: SCSCP and POPCORN
- Packaging Mathematical Structures
- Project abstract: logic atlas and integrator (LATIN)
- Representing model theory in a type-theoretical logical framework
- Specifications in an arbitrary institution
- Structured theory presentations and logic representations
- The Mizar Mathematical Library in OMDoc: translation and applications
- The TPTP problem library. CNF release v1. 2. 1
- The calculus of constructions
- Towards MKM in the large: modular representation and scalable software architecture
- Towards a mechanized metatheory of Standard ML
- Towards logical frameworks in the heterogeneous tool set Hets
Cited in
(46)- The future of logic: foundation-independence
- A web-based toolkit for mathematical word processing applications with semantics
- SpeX: a rewriting-based formal specification environment
- Math Literate Knowledge Management via Induced Material
- Theory presentation combinators
- Towards Knowledge Management for HOL Light
- Mathematical models as research data via flexiformal theory graphs
- Compensating the Computational Bias of Spreadsheets with MKM Techniques
- Combining source, content, presentation, narration, and relational representation
- The SMGloM Project and System: Towards a Terminology and Ontology for Mathematics
- Formal logic definitions for interchange languages
- Structure-preserving diagram operators
- Diagram combinators in MMT
- A new export of the Mizar mathematical library
- System description STEX3 -- a \LaTeX-based ecosystem for semantic/active mathematical documents
- Towards MKM in the large: modular representation and scalable software architecture
- A data model and encoding for a semantic, multilingual terminology of mathematics
- Flexary operators for formalized mathematics
- A query language for formal mathematical libraries
- A foundational view on integration problems
- Spreadsheet Interaction with Frames: Exploring a Mathematical Practice
- Project abstract: logic atlas and integrator (LATIN)
- Generic literals
- The Mizar Mathematical Library in OMDoc: translation and applications
- Classification of alignments between concepts of formal mathematical systems
- Lax theory morphisms
- scientific article; zbMATH DE number 7756106 (Why is no real title available?)
- LF+ in Coq for "fast and loose" reasoning
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- Injecting formal mathematics into LaTeX
- Realms: a structure for consolidating knowledge about mathematical theories
- Discourse-level parallel markup and meaning adoption in flexiformal theory graphs
- A logical framework perspective on conservativity
- Reusing learning objects via theory morphisms
- Semantics of \textsc{OpenMath} and \textsc{MathML3}
- Experiences from exporting major proof assistant libraries
- A flexiformal model of knowledge dissemination and aggregation in mathematics
- Making PVS accessible to generic services by interpretation in a universal format
- Structuring theories with implicit morphisms
- The MMT API: a generic MKM system
- Interoperability in the OpenDreamKit project: the math-in-the-middle approach
- System description: MathHub.info
- Virtual theories -- a uniform interface to mathematical knowledge bases
- Extracting theory graphs from Aldor libraries
- Morphism equality in theory graphs
- Formalizing mathematical knowledge as a biform theory graph: a case study
Describes a project that uses
Uses Software
This page was built for publication: A scalable module system
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q391632)
