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