| Publication | Date of Publication | Type |
|---|
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?)
| 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
| 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 |
