| Publication | Date of Publication | Type |
|---|
| The dependently typed higher-order form for the TPTP world | 2026-02-26 | Paper |
| Subtyping in dependently-typed higher-order logic | 2026-02-26 | Paper |
| Global, regional, and local contexts | 2026-02-19 | Paper |
| Lightweight realms | 2026-02-19 | Paper |
Dependently typed higher-order logic
ACM Transactions on Computational Logic | 2026-01-07 | Paper |
| Rapid prototyping formal systems in MMT: 5 case studies | 2025-08-19 | Paper |
| Systematic translation of formalizations of type theory from intrinsic to extrinsic style | 2025-08-19 | Paper |
| Representing Isabelle in LF | 2025-08-19 | Paper |
| A logical framework perspective on conservativity | 2024-12-04 | Paper |
Morphism equality in theory graphs
Lecture Notes in Computer Science | 2024-02-28 | Paper |
Extracting theory graphs from Aldor libraries
Lecture Notes in Computer Science | 2024-02-28 | Paper |
scientific article; zbMATH DE number 7756106 (Why is no real title available?)
(available as arXiv preprint) | 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
Journal of Automated Reasoning | 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
The Mathematical Intelligencer | 2021-04-19 | Paper |
A survey of languages for formalizing mathematics
(available as arXiv preprint) | 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
Recent Trends in Algebraic Development Techniques | 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
Mathematical Aspects of Computer and Information Sciences | 2019-03-14 | Paper |
Knowledge-based interoperability for mathematical software systems
Mathematical Aspects of Computer and Information Sciences | 2019-03-14 | Paper |
A Modular Type Reconstruction Algorithm
ACM Transactions on Computational Logic | 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?
Journal Of Logic And Computation | 2018-02-13 | Paper |
| Making PVS accessible to generic services by interpretation in a universal format | 2018-01-04 | Paper |
Morphism axioms
Theoretical Computer Science | 2017-09-07 | Paper |
| Classification of alignments between concepts of formal mathematical systems | 2017-07-21 | Paper |
Lax theory morphisms
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Interoperability in the OpenDreamKit project: the math-in-the-middle approach
Lecture Notes in Computer Science | 2016-08-30 | Paper |
The future of logic: foundation-independence
Logica Universalis | 2016-04-04 | Paper |
Generic literals
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Formal logic definitions for interchange languages
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Logical relations for a logical framework
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Towards Knowledge Management for HOL Light
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Flexary operators for formalized mathematics
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Representing model theory in a type-theoretical logical framework
Electronic Notes in Theoretical Computer Science | 2014-07-23 | Paper |
A logical framework combining model and proof theory
Mathematical Structures in Computer Science | 2014-03-12 | Paper |
A scalable module system
Information and Computation | 2014-01-10 | Paper |
Compiling logics
Recent Trends in Algebraic Development Techniques | 2013-09-13 | Paper |
The MMT API: a generic MKM system
Lecture Notes in Computer Science | 2013-08-09 | Paper |
A universal machine for biform theory graphs
Lecture Notes in Computer Science | 2013-08-09 | Paper |
Semantics of \textsc{OpenMath} and \textsc{MathML3}
Mathematics in Computer Science | 2013-04-24 | Paper |
The Mizar Mathematical Library in OMDoc: translation and applications
Journal of Automated Reasoning | 2013-04-17 | Paper |
Extending MKM formats at the statement level
Lecture Notes in Computer Science | 2012-09-07 | Paper |
A query language for formal mathematical libraries
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Management of Change in Declarative Languages
Lecture Notes in Computer Science | 2012-09-07 | Paper |
A proof theoretic interpretation of model theoretic hiding
Recent Trends in Algebraic Development Techniques | 2012-06-08 | Paper |
Towards logical frameworks in the heterogeneous tool set Hets
Recent Trends in Algebraic Development Techniques | 2012-06-08 | Paper |
Kripke Semantics for Martin-L\"of's Extensional Type Theory
Logical Methods in Computer Science | 2012-04-02 | Paper |
Representing model theory in a type-theoretical logical framework
Theoretical Computer Science | 2011-12-23 | Paper |
Formalising foundations of mathematics
Mathematical Structures in Computer Science | 2011-10-21 | Paper |
Project abstract: logic atlas and integrator (LATIN)
Lecture Notes in Computer Science | 2011-07-29 | Paper |
A foundational view on integration problems
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Combining source, content, presentation, narration, and relational representation
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Towards MKM in the large: modular representation and scalable software architecture
Lecture Notes in Computer Science | 2010-08-24 | Paper |
Translating a Dependently-Typed Logic to First-Order Logic
Recent Trends in Algebraic Development Techniques | 2009-10-22 | Paper |
Integrating Web Services into Active Mathematical Documents
Lecture Notes in Computer Science | 2009-07-09 | Paper |
Kripke Semantics for Martin-Löf’s Extensional Type Theory
Lecture Notes in Computer Science | 2009-07-07 | Paper |
Solving the \$100 modal logic challenge
Journal of Applied Logic | 2009-03-25 | Paper |
First-Order Logic with Dependent Types
Automated Reasoning | 2009-03-12 | Paper |
Notations for Living Mathematical Documents
Lecture Notes in Computer Science | 2009-01-27 | Paper |
THF0 – The Core of the TPTP Language for Higher-Order Logic
Automated Reasoning | 2008-11-27 | Paper |
