Please respect any copyrights when downloading

- [2] (2013) The Mizar Mathematical Library in OMDoc: translation and applications. Journal of Automated Reasoning 50 (2), pp. 191–202. External Links: Link, Document Cited by: p1.
- [3] (2013) A scalable module system. Information & Computation 0 (230), pp. 1–54. External Links: Link Cited by: p1.
- [4] (2013) Logical Relations for a Logical Framework. ACM Transactions on Computational Logic. External Links: Link Cited by: p1.
- [1] (2011) Representing Model Theory in a Type-Theoretical Logical Framework. Theoretical Computer Science 412 (37), pp. 4919–4945. Cited by: p1.

- [8] (2013) A universal machine for biform theory graphs. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.), Lecture Notes in Computer Science. External Links: Link Cited by: p1.
- [6] (2012) Extending MKM formats at the statement level. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 65–80. External Links: Link Cited by: p1.
- [7] (2012) Management of Change in Declarative Languages. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 325–340. Cited by: p1.
- [11] (2012) A Query Language for Formal Mathematical Libraries. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 142–157. External Links: 1204.4685 Cited by: p1.
- [1] (2011) A Proof Theoretic Interpretation of Model Theoretic Hiding. In Recent Trends in Algebraic Development TechniquesRecent Trends in Algebraic Development Techniques, H. Kreowski and T. Mossakowski (Eds.), LNCS. Cited by: p1.
- [2] (2011) Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In Recent Trends in Algebraic Development TechniquesRecent Trends in Algebraic Development Techniques, H. Kreowski and T. Mossakowski (Eds.), LNCS. Cited by: p1.
- [3] (2011) Project abstract: logic atlas and integrator (LATIN). In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 289–291. External Links: Link, Document Cited by: p1.
- [4] (2011) Combining source, content, presentation, narration, and relational representation. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 212–227. External Links: Link Cited by: p1.
- [5] (2011) Extending OpenMath with Sequences. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 58–72. External Links: Link Cited by: p1.
- [9] (2011) A foundational view on integration problems. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 107–122. Note: https://kwarc.info/kohlhase/papers/cicm11-integration.pdf External Links: Link Cited by: p1.
- [10] (2010) Towards MKM in the large: modular representation and scalable software architecture. In Intelligent computer mathematicsIntelligent Computer Mathematics, S. Autexier, J. Calmet, D. Delahaye, P. D. F. Ion, L. Rideau, R. Rioboo, and A. P. Sexton (Eds.), LNAI, pp. 370–384. External Links: 1005.5232v2 Cited by: p1.
- [13] (2010) A [insert xml format] database for [insert cool application]. In Proceedings of XML Prague 2010Proceedings of XML Prague 2010, External Links: Link Cited by: p1.
- [12] (2009) Translating Dependently-Typed Logic to First-Order Logic. In Recent Trends in Algebraic Development Techniques, A. Corradini and U. Montanari (Eds.), LNCS, Vol. 5486, pp. 326–341. Cited by: p1.

- [1] (2014-11) A framework for defining declarative languages. Ph.D. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
- [2] (2012) Management of change in declarative languages. Master’s Thesis, Jacobs University Bremen. Cited by: p1.
- [3] (2010) Mechanically Verifying Logic Translations. Master’s Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.

- [9] (2021) A Language with Type-Dependent Equality. In Intelligent Computer Mathematics, F. Kamareddine and C. Sacerdoti Coen (Eds.), pp. 211–227. External Links: Document, Link Cited by: p1.
- [12] (2021) Systematic translation of formalizations of type theory from intrinsic to extrinsic style. In Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), E. Pimentel and E. Tassi (Eds.), External Links: Link, Document Cited by: p1.
- [1] (2012) Representing CASL in a Proof-Theoretical Logical Framework. In Workshop on Algebraic Development Techniques, Cited by: p1.
- [3] (2012) Compiling Logics. In Workshop on Algebraic Development Techniques, Cited by: p1.
- [6] (2012) Representing Categories of Theories in a Proof-Theoretical Logical Framework. In Workshop on Algebraic Development Techniques, Cited by: p1.
- [7] (2012) Management of Change in Declarative Languages. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 325–340. Cited by: p1.
- [14] (2012) Mechanically Verifying Logic Translations. In Workshop on Algebraic Development Techniques, Cited by: p1.
- [17] (2012) A Query Language for Formal Mathematical Libraries. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 142–157. External Links: 1204.4685 Cited by: p1.
- [2] (2011) Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In Recent Trends in Algebraic Development TechniquesRecent Trends in Algebraic Development Techniques, H. Kreowski and T. Mossakowski (Eds.), LNCS. Cited by: p1.
- [5] (2011) Extending OpenMath with Sequences. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 58–72. External Links: Link Cited by: p1.
- [16] (2010) Representing Isabelle in LF. In Logical Frameworks and Meta-languages: Theory and Practice, K. Crary and M. Miculan (Eds.), Electronic Proceedings in Theoretical Computer Science, Vol. 34, pp. 85–100. Cited by: p1.
- [18] (2010) A [insert xml format] database for [insert cool application]. In Proceedings of XML Prague 2010Proceedings of XML Prague 2010, External Links: Link Cited by: p1.
- [8]
(2009-07)
Semantics of OpenMath and MathML3.
In 22
^{nd}openmath workshop22^{nd}OpenMath Workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1. - [11]
(2009-07)
A better role system for OpenMath.
In 22
^{nd}openmath workshop22^{nd}OpenMath Workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1. - [4] (2009) Representing Model Theory in a Type-Theoretical Logical Framework. In Fourth Workshop on Logical and Semantic Frameworks, with Applications, M. Ayala-Rincón and F. Kamareddine (Eds.), Electronic Notes in Theoretical Computer Science, Vol. 256, pp. 49–65. Cited by: p1.
- [13] (2009) A Practical Module System for LF. In Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), J. Cheney and A. Felty (Eds.), ACM International Conference Proceeding Series, Vol. LFMTP’09, pp. 40–48. Cited by: p1.
- [15] (2009) Representing Logics and Logic Translations. In Ausgezeichnete Informatikdissertationen 2008, D. Wagner et al. (Ed.), Lecture Notes in Informatics, Vol. D-9, pp. 201–210. Note: English title: Outstanding Dissertations in Computer Science 2008 Cited by: p1.
- [10]
(2008)
An exchange format for modular knowledge.
In Proceedings of the LPAR Workshops: Knowledge Exchange:
Automated Provers and Proof Assistants, and The 7
^{th}International Workshop on the Implementation of Logics, G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz (Eds.), CEUR Workshop Proceedings, Aachen, pp. 50–68. External Links: ISSN 1613-0073 Cited by: p1.

- [1] (2011) Translating the Mizar Mathematical Library into OMDoc format. KWARC Report Jacobs University Bremen. Note: http://uniformal.github.io/doc/applications/LATIN/docs/Mizar2OMDoc-Report.pdf External Links: Link Cited by: p1.
- [2] (2010) A [insert xml format] database for [insert cool application] (extended version). Technical report Jacobs University Bremen. Note: https://kwarc.info/vzholudev/pubs/XMLPrague_long.pdf External Links: Link Cited by: p1.

- [5] (2021-03-22) A beginner’s guide to logical relations for a logical framework. seminar paper, FAU Erlangen-Nürnberg. Note: written as a student of the kwarc seminar External Links: Link Cited by: p1.
- [4] (2021-01-27) A beginner’s guide to logical relations for a logical framework (slides). seminar presentation, FAU Erlangen-Nürnberg. Note: presented as a student of the kwarc seminar External Links: Link Cited by: p1.
- [3] (2021) Modular formalization of formal systems. Note: under review External Links: Link Cited by: p1.
- [1] (2010) Towards an atlas of logics. External Links: Link Cited by: p1.
- [2] (2010) A Formalized Set-Theoretical Semantics of Isabelle/HOL. External Links: Link Cited by: p1.