Publication | Date of Publication | Type |
---|
Morphism equality in theory graphs | 2024-02-28 | Paper |
Extracting theory graphs from Aldor libraries | 2024-02-28 | Paper |
https://portal.mardi4nfdi.de/entity/Q6079227 | 2023-10-27 | Paper |
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint | 2023-05-24 | Paper |
Logic-independent proof search in logical frameworks (short paper) | 2022-11-09 | Paper |
A new export of the Mizar mathematical library | 2022-04-22 | Paper |
A language with type-dependent equality | 2022-04-22 | Paper |
Experiences from exporting major proof assistant libraries | 2022-01-21 | Paper |
Structure-preserving diagram operators | 2021-10-27 | Paper |
Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge | 2021-04-19 | Paper |
Towards a heterogeneous query language for mathematical knowledge | 2021-01-20 | Paper |
A survey of languages for formalizing mathematics | 2021-01-20 | Paper |
Representing structural language features in formal meta-languages | 2021-01-20 | Paper |
TGView3D: a system for 3-dimensional visualization of theory graphs | 2021-01-20 | Paper |
Structuring theories with implicit morphisms | 2020-06-08 | Paper |
Towards a unified mathematical data infrastructure: database and interface generation | 2020-01-22 | Paper |
Relational data across mathematical libraries | 2020-01-22 | Paper |
The Coq library as a theory graph | 2020-01-22 | Paper |
MMTTeX: connecting content and narration-oriented document formats | 2020-01-22 | Paper |
Diagram combinators in MMT | 2020-01-22 | Paper |
Integrating semantic mathematical documents and dynamic notebooks | 2020-01-22 | Paper |
Canonical Selection of Colimits | 2020-01-16 | Paper |
QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge | 2019-09-18 | Paper |
Knowledge-Based Interoperability for Mathematical Software Systems | 2019-03-14 | Paper |
Virtual Theories – A Uniform Interface to Mathematical Knowledge Bases | 2019-03-14 | Paper |
A Modular Type Reconstruction Algorithm | 2019-02-07 | Paper |
Automatically finding theory morphisms for knowledge management | 2018-10-18 | Paper |
Theories as types | 2018-10-18 | Paper |
How to identify, translate and combine logics? | 2018-02-13 | Paper |
Making PVS accessible to generic services by interpretation in a universal format | 2018-01-04 | Paper |
Morphism axioms | 2017-09-07 | Paper |
Classification of alignments between concepts of formal mathematical systems | 2017-07-21 | Paper |
Lax Theory Morphisms | 2017-07-12 | Paper |
Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach | 2016-08-30 | Paper |
The future of logic: foundation-independence | 2016-04-04 | Paper |
Generic Literals | 2015-11-20 | Paper |
Formal Logic Definitions for Interchange Languages | 2015-11-20 | Paper |
Logical relations for a logical framework | 2015-09-17 | Paper |
Flexary Operators for Formalized Mathematics | 2014-08-07 | Paper |
Towards Knowledge Management for HOL Light | 2014-08-07 | Paper |
Representing Model Theory in a Type-Theoretical Logical Framework | 2014-07-23 | Paper |
A logical framework combining model and proof theory | 2014-03-12 | Paper |
A scalable module system | 2014-01-10 | Paper |
Compiling Logics | 2013-09-13 | Paper |
A Universal Machine for Biform Theory Graphs | 2013-08-09 | Paper |
The MMT API: A Generic MKM System | 2013-08-09 | Paper |
Semantics of \textsc{OpenMath} and \textsc{MathML3} | 2013-04-24 | Paper |
The Mizar Mathematical Library in OMDoc: translation and applications | 2013-04-17 | Paper |
Extending MKM Formats at the Statement Level | 2012-09-07 | Paper |
A Query Language for Formal Mathematical Libraries | 2012-09-07 | Paper |
Management of Change in Declarative Languages | 2012-09-07 | Paper |
A Proof Theoretic Interpretation of Model Theoretic Hiding | 2012-06-08 | Paper |
Towards Logical Frameworks in the Heterogeneous Tool Set Hets | 2012-06-08 | Paper |
Kripke Semantics for Martin-L\"of's Extensional Type Theory | 2012-04-02 | Paper |
Representing model theory in a type-theoretical logical framework | 2011-12-23 | Paper |
Formalising foundations of mathematics | 2011-10-21 | Paper |
A Foundational View on Integration Problems | 2011-07-29 | Paper |
Combining Source, Content, Presentation, Narration, and Relational Representation | 2011-07-29 | Paper |
Project Abstract: Logic Atlas and Integrator (LATIN) | 2011-07-29 | Paper |
Towards MKM in the Large: Modular Representation and Scalable Software Architecture | 2010-08-24 | Paper |
Translating a Dependently-Typed Logic to First-Order Logic | 2009-10-22 | Paper |
Integrating Web Services into Active Mathematical Documents | 2009-07-09 | Paper |
Kripke Semantics for Martin-Löf’s Extensional Type Theory | 2009-07-07 | Paper |
Solving the \$100 modal logic challenge | 2009-03-25 | Paper |
First-Order Logic with Dependent Types | 2009-03-12 | Paper |
Notations for Living Mathematical Documents | 2009-01-27 | Paper |
THF0 – The Core of the TPTP Language for Higher-Order Logic | 2008-11-27 | Paper |