| Publication | Date of Publication | Type |
|---|
| A logical framework perspective on conservativity | 2024-12-04 | Paper |
| 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 |
| A survey of languages for formalizing mathematics | 2021-01-20 | Paper |
| Representing structural language features in formal meta-languages | 2021-01-20 | Paper |
| Towards a heterogeneous query language for mathematical knowledge | 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 |
| MMTTeX: connecting content and narration-oriented document formats | 2020-01-22 | Paper |
| Relational data across mathematical libraries | 2020-01-22 | Paper |
| The Coq library as a theory graph | 2020-01-22 | Paper |
| Diagram combinators in MMT | 2020-01-22 | Paper |
| Towards a unified mathematical data infrastructure: database and interface generation | 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 |
| Virtual Theories – A Uniform Interface to Mathematical Knowledge Bases | 2019-03-14 | Paper |
| Knowledge-Based Interoperability for Mathematical Software Systems | 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 |
| Towards Knowledge Management for HOL Light | 2014-08-07 | Paper |
| Flexary Operators for Formalized Mathematics | 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 |
| The MMT API: A Generic MKM System | 2013-08-09 | Paper |
| A Universal Machine for Biform Theory Graphs | 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 |
| Project Abstract: Logic Atlas and Integrator (LATIN) | 2011-07-29 | Paper |
| A Foundational View on Integration Problems | 2011-07-29 | Paper |
| Combining Source, Content, Presentation, Narration, and Relational Representation | 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 |
