Project MMT (Meta Meta Theories/Toolkit) : Selected Publications

Please respect any copyrights when downloading
  1. Archival Literature
    1. Articles in Journals
    2. Papers at International, Peer-Reviewed Conferences
  2. Theses
  3. Gray Literature
    1. Papers at Peer-Reviewed Workshops
    2. Technical Reports
  4. Unpublished
  5. Miscellaneous

Archival Literature

Articles in Journals

  1. [6] T. Koprucki, M. Kohlhase, K. Tabelow, D. Müller, and F. Rabe (2018) Model pathway diagrams for the representation of mathematical models. Journal of Optical and Quantum Electronics 50 (2), pp. 70. External Links: Document Cited by: p1.
  2. [12] F. Rabe (2017) How to Identify, Translate, and Combine Logics?. Journal of Logic and Computation 27 (6), pp. 1753–1798. Cited by: p1.
  3. [13] F. Rabe (2017) Morphism Axioms. Theoretical Computer Science 691, pp. 55–80. Cited by: p1.
  4. [5] M. Kohlhase and F. Rabe (2016) QED reloaded: towards a pluralistic formal library of mathematical knowledge. Journal of Formalized Reasoning 9 (1), pp. 201–234. External Links: Link Cited by: p1.
  5. [11] F. Rabe (2015) The Future of Logic: Foundation-Independence. Logica Universalis 10 (1), pp. 1–20. Note: Winner of the Contest “The Future of Logic” at the World Congress on Universal Logic External Links: Document, Link Cited by: p1.
  6. [3] M. Iancu, M. Kohlhase, F. Rabe, and J. Urban (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.
  7. [7] F. Rabe and M. Kohlhase (2013) A scalable module system. Information & Computation 0 (230), pp. 1–54. External Links: Link Cited by: p1.
  8. [10] F. Rabe (2013) A Logical Framework Combining Model and Proof Theory. Mathematical Structures in Computer Science 23 (5), pp. 945–1001. Cited by: p1.
  9. [9] F. Rabe (2012) A logical framework combining model and proof theory. Mathematical Structures in Computer Science. External Links: Link Cited by: p1.
  10. [2] F. Horozal and F. Rabe (2011) Representing Model Theory in a Type-Theoretical Logical Framework. Theoretical Computer Science 412 (37), pp. 4919–4945. Cited by: p1.
  11. [4] M. Iancu and F. Rabe (2011) Formalizing Foundations of Mathematics. Mathematical Structures in Computer Science 21 (4), pp. 883–911. External Links: Document, Link Cited by: p1.
  12. [1] J. Goguen, T. Mossakowski, V. de Paiva, F. Rabe, and L. Schröder (2008) An Institutional View on Categorical Logic. International Journal of Software and Informatics 1 (1), pp. 129–152. Cited by: p1.
  13. [8] F. Rabe, P. Pudlák, G. Sutcliffe, and W. Shen (2007) Solving the $100 Modal Logic Challenge. Journal of Applied Logic 1 (1). Cited by: p1.

Papers at International, Peer-Reviewed Conferences

  1. [14] M. Kohlhase, B. Bösl, R. Marcus, D. Müller, D. Rochau, N. Roux, J. Schihada, and M. Stamminger (2020) FrameIT: detangling knowledge management from game design in serious games. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2020, C. Benzmüller and B. Miller (Eds.), LNAI, Vol. 12236, pp. 173–189. External Links: Document, Link Cited by: p1.
  2. [22] R. Marcus, M. Kohlhase, and F. Rabe (2020) TGView3D: a system for 3-dimensional visualization of theory graphs. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2020, C. Benzmüller and B. Miller (Eds.), LNAI, Vol. 12236, pp. 290–296. External Links: Link Cited by: p1.
  3. [25] D. Müller, F. Rabe, C. Rothgang, and M. Kohlhase (2020) Representing structural language features in formal meta-languages. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2020, C. Benzmüller and B. Miller (Eds.), LNAI, Vol. 12236, pp. 206–221. External Links: Link Cited by: p1.
  4. [29] J. F. Schaefer, K. Amann, and M. Kohlhase (2020) Prototyping controlled mathematical languages in jupyter notebooks. In Mathematical software – icms 2020. 7th international conferenceMathematical Software – ICMS 2020. 7th international conference, A. M. Bigatti, J. Carette, J. H. Davenport, M. Joswig, and T. de Wolff (Eds.), LNCS, Vol. 12097, pp. 406–415. External Links: Link Cited by: p1.
  5. [24] D. Müller, F. Rabe, and M. Kohlhase (2018) Theories as types. In 9th international joint conference on automated reasoning9th International Joint Conference on Automated Reasoning, D. Galmiche, S. Schulz, and R. Sebastiani (Eds.), External Links: Link Cited by: p1.
  6. [26] T. Pollinger, M. Kohlhase, and H. Köstler (2018) Knowledge amalgamation for computational science and engineering. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2018, F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.), LNAI. External Links: Link Cited by: p1.
  7. [18] M. Kohlhase, D. Müller, S. Owre, and F. Rabe (2017) Making PVS accessible to generic services by interpretation in a universal format. In Interactive theorem proving 8th international conference, itp 2017Interactive Theorem Proving, M. Ayala-Rincón and C. A. Muñoz (Eds.), LNCS, Vol. 10499. External Links: Link Cited by: p1.
  8. [19] M. Kohlhase, D. Müller, M. Pfeiffer, F. Rabe, N. Thiéry, V. Vasilyev, and T. Wiesing (2017) Knowledge-based interoperability for mathematical software systems. In MACIS 2017MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences, J. Blömer, T. Kutsia, and D. Simos (Eds.), LNCS, pp. 195–210. External Links: Link Cited by: p1.
  9. [23] D. Müller, T. Gauthier, C. Kaliszyk, M. Kohlhase, and F. Rabe (2017) Classification of alignments between concepts of formal mathematical systems. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2017, H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke (Eds.), LNAI. External Links: Link Cited by: p1.
  10. [31] T. Wiesing, M. Kohlhase, and F. Rabe (2017) Virtual theories – a uniform interface to mathematical knowledge bases. In MACIS 2017MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences, J. Blömer, T. Kutsia, and D. Simos (Eds.), LNCS, pp. 243–257. External Links: Link Cited by: p1.
  11. [6] P. Dehaye, M. Iancu, M. Kohlhase, A. Konovalov, S. Lelièvre, D. Müller, M. Pfeiffer, F. Rabe, N. M. Thiéry, and T. Wiesing (2016) Interoperability in the OpenDreamKit project: the math-in-the-middle approach. In Intelligent computer mathematicsIntelligent Computer Mathematics 2016, M. Kohlhase, M. Johansson, B. Miller, L. de Moura, and F. Tompa (Eds.), LNAI. External Links: Link Cited by: p1.
  12. [10] F. Horozal, M. Kohlhase, and F. Rabe (2014) Flexary operators for formalized mathematics. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 312–327. External Links: Link Cited by: p1.
  13. [11] M. Iancu, M. Kohlhase, and C. Prodescu (2014) Representing, archiving, and searching the space of mathematical knowledge. In Mathematical software - ICMS 2014 - 4th international congressMathematical Software - ICMS 2014 - 4th International Congress, H. Hong and C. Yap (Eds.), LNCS, Vol. 8592, pp. 26–30. External Links: Document, Link Cited by: p1.
  14. [13] C. Kaliszyk and F. Rabe (2014) Towards knowledge management for HOL Light. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 357–372. External Links: Link Cited by: p1.
  15. [15] M. Kohlhase and M. Iancu (2014) Discourse-level parallel markup and meaning adoption in flexiformal theory graphs. In Mathematical software - ICMS 2014 - 4th international congressMathematical Software - ICMS 2014 - 4th International Congress, H. Hong and C. Yap (Eds.), LNCS, Vol. 8592, pp. 36–40. External Links: Document Cited by: p1.
  16. [16] M. Kohlhase, F. Mance, and F. Rabe (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.
  17. [28] F. Rabe (2013) The MMT API: A Generic MKM System. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.), Lecture Notes in Computer Science, pp. 339–343. Cited by: p1.
  18. [9] F. Horozal, M. Kohlhase, and F. Rabe (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.
  19. [12] M. Iancu and F. Rabe (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.
  20. [27] F. Rabe (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.
  21. [1] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, and F. Rabe (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.
  22. [2] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, F. Rabe, and K. Sojakova (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.
  23. [3] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, and F. Rabe (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.
  24. [8] F. Horozal, A. Iacob, C. Jucovschi, M. Kohlhase, and F. Rabe (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.
  25. [20] M. Kohlhase, F. Rabe, and C. Sacerdoti Coen (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.
  26. [4] C. David, C. Lange, and F. Rabe (2010) Interactive Documents as Interfaces to Computer Algebra Systems: JOBAD and Wolfram—Alpha. In CALCULEMUS (Emerging Trends), D. Delahaye and R. Rioboo (Eds.), Technical Reports of CEDRIC (CNAM/ENSIIE), pp. 13–30. Cited by: p1.
  27. [5] C. David, M. Kohlhase, C. Lange, F. Rabe, N. Zhiltsov, and V. Zholudev (2010) Publishing math lecture notes as linked data. In The semantic web: research and applications (part II)The Semantic Web: Research and Applications (Part II), L. Aroyo, G. Antoniou, E. Hyvönen, A. ten Teije, H. Stuckenschmidt, L. Cabral, and T. Tudorache (Eds.), LNCS, pp. 370–375. External Links: 1004.3390v1 Cited by: p1.
  28. [21] M. Kohlhase, F. Rabe, and V. Zholudev (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.
  29. [32] V. Zholudev, M. Kohlhase, and F. Rabe (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.
  30. [7] J. Gičeva, C. Lange, and F. Rabe (2009-07) Integrating web services into active mathematical documents. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI, pp. 279–293. External Links: Link Cited by: p1.
  31. [30] K. Sojakova and F. Rabe (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.
  32. [17] M. Kohlhase, C. Müller, and F. Rabe (2008) Notations for living mathematical documents. In Intelligent computer mathematicsIntelligent Computer Mathematics, S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. Suzuki, and F. Wiedijk (Eds.), LNAI, pp. 504–519. External Links: Link Cited by: p1.

Theses

  1. [5] D. Müller (2019-12) Mathematical knowledge management across formal libraries. Ph.D. Thesis, Informatics, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  2. [1] F. Horozal (2014-11) A framework for defining declarative languages. Ph.D. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  3. [4] F. Mance (2013) A Practical OpenMath Machine. Master’s Thesis, Jacobs University Bremen. Note: Bachelor’s thesis Cited by: p1.
  4. [3] M. Iancu (2012) Management of change in declarative languages. Master’s Thesis, Jacobs University Bremen. Cited by: p1.
  5. [2] A. Iacob (2011-08) Towards Project-Based Workflows in Twelf. Master’s Thesis, Jacobs University Bremen, Bremen, Germany. External Links: Link Cited by: p1.
  6. [7] K. Sojakova (2010) Mechanically Verifying Logic Translations. Master’s Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  7. [6] F. Rabe (2008) Representing Logics and Logic Translations. Ph.D. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.

Gray Literature

Papers at Peer-Reviewed Workshops

  1. [24] F. Rabe (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.
  2. [28] F. Rabe and N. Roux (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.
  3. [42] N. Roux and F. Rabe (2021) Structure-Preserving Diagram Operators. In Recent Trends in Algebraic Development Techniques, M. Roggenbach (Ed.), Lecture Notes in Computer Science, Vol. 12669, pp. 142–163. External Links: Link, ISBN 978-3-030-73785-6, Document Cited by: p1.
  4. [43] J. F. Schaefer, K. Amann, and M. Kohlhase (2020) Prototyping controlled mathematical languages in jupyter notebooks. In Mathematical software – icms 2020. 7th international conferenceMathematical Software – ICMS 2020. 7th international conference, A. M. Bigatti, J. Carette, J. H. Davenport, M. Joswig, and T. de Wolff (Eds.), LNCS, Vol. 12097, pp. 406–415. External Links: Link Cited by: p1.
  5. [44] J. F. Schaefer and M. Kohlhase (2020) GLIF: a declarative framework for symbolic natural language understanding. In Proceedings of the 6th Workshop on Formal and Cognitive Reasoning, C. Beierle, M. Ragni, F. Stolzenburg, and M. Thimm (Eds.), pp. 4–11. External Links: Link Cited by: p1.
  6. [22] D. Müller, F. Rabe, and M. Kohlhase (2018) Theories as types. In 9th international joint conference on automated reasoning9th International Joint Conference on Automated Reasoning, D. Galmiche, S. Schulz, and R. Sebastiani (Eds.), External Links: Link Cited by: p1.
  7. [27] F. Rabe and D. Müller (2018) Structuring theories with implicit morphisms. In 24th International Workshop on Algebraic Development Techniques 2018, External Links: Link Cited by: p1.
  8. [23] D. Müller, C. Rothgang, Y. Liu, and F. Rabe (2017) Alignment-based translations across formal systems using interface theories. In Fifth Workshop on Proof eXchange for Theorem Proving - PxTP 2017, External Links: Link Cited by: p1.
  9. [40] F. Rabe (2017) The MMT Perspective on Conservativity. In Logical and Semantic Frameworks, with Applications, S. Alves and R. Wassermann (Eds.), pp. 17–33. Cited by: p1.
  10. [17] C. Kaliszyk, M. Kohlhase, D. Müller, and F. Rabe (2016) A standard for aligning mathematical concepts. In Intelligent computer mathematics – work in progress papersIntelligent Computer Mathematics – Work in Progress Papers, M. Kohlhase, A. Kohlhase, P. Libbrecht, B. Miller, A. Naumowicz, W. Neuper, P. Quaresma, F. Tompa, and M. Suda (Eds.), External Links: Link Cited by: p1.
  11. [20] R. Kumar and F. Rabe (2016) Breakout session on A standard for system integration and proof interchange. In Dagstuhl Seminar on Universality of Proofs, G. Dowek, C. Dubois, B. Pientka, and F. Rabe (Eds.), pp. 94–94. Cited by: p1.
  12. [39] F. Rabe (2016) MMT: A UniFormal Approach to Knowledge Representation. In Dagstuhl Seminar on Universality of Proofs, G. Dowek, C. Dubois, B. Pientka, and F. Rabe (Eds.), pp. 88–88. Cited by: p1.
  13. [41] D. Rochau, M. Kohlhase, and D. Müller (2016) FrameIT reloaded: serious math games from modular math ontologies. In Intelligent computer mathematics – work in progress papersIntelligent Computer Mathematics – Work in Progress Papers, M. Kohlhase, A. Kohlhase, P. Libbrecht, B. Miller, A. Naumowicz, W. Neuper, P. Quaresma, F. Tompa, and M. Suda (Eds.), External Links: Link Cited by: p1.
  14. [11] F. Horozal and F. Rabe (2015) Formal Logic Definitions for Interchange Languages. In Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge (Eds.), pp. 171–186. Cited by: p1.
  15. [38] F. Rabe (2015) Generic Literals. In Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge (Eds.), pp. 102–117. Cited by: p1.
  16. [12] F. Horozal, M. Kohlhase, and F. Rabe (2014) Flexary operators for formalized mathematics. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 312–327. External Links: Link Cited by: p1.
  17. [18] C. Kaliszyk and F. Rabe (2014) Towards knowledge management for HOL Light. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 357–372. External Links: Link Cited by: p1.
  18. [19] M. Kohlhase (2014) OpenMath language extensions. In Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2014MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, M. England, J. H. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper, P. Quaresma, A. P. Sexton, P. Sojka, J. Urban, and S. M. Watt (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  19. [35] F. Rabe (2014) A Logic-Independent IDE. In Workshop on user interfaces for theorem proversWorkshop on User Interfaces for Theorem Provers, C. Benzmüller and B. Woltzenlogel Paleo (Eds.), pp. 48–60. External Links: Link Cited by: p1.
  20. [36] F. Rabe (2014) A Logic-Independent IDE. In Workshop on User Interfaces for Theorem Provers, C. Benzmüller and B. Woltzenlogel Paleo (Eds.), pp. 48–60. External Links: Document Cited by: p1.
  21. [37] F. Rabe (2014) MMT Objects. In Workshops and Work in Progress at CICM 2014: OpenMath Workshop, M. England, J. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper, P. Quaresma, A. Sexton, P. Sojka, J. Urban, and S. Watt (Eds.), Cited by: p1.
  22. [14] M. Iancu, F. Mance, and F. Rabe (2013) The Scala-REPL + MMT as a lightweight mathematical user interface. In Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2013MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, C. Lange, D. Aspinall, J. Carette, J. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, P. Quaresma, F. Rabe, P. Sojka, I. Whiteside, and W. Windsteiger (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  23. [2] M. Codescu, F. Horozal, I. Ignatov, and F. Rabe (2012) Representing CASL in a Proof-Theoretical Logical Framework. In Workshop on Algebraic Development Techniques, Cited by: p1.
  24. [4] M. Codescu, F. Horozal, T. Mossakowski, and F. Rabe (2012) Compiling Logics. In Workshop on Algebraic Development Techniques, Cited by: p1.
  25. [13] F. Horozal and F. Rabe (2012) Representing Categories of Theories in a Proof-Theoretical Logical Framework. In Workshop on Algebraic Development Techniques, Cited by: p1.
  26. [15] M. Iancu and F. Rabe (2012) (Work-in-Progress) An MMT-Based User-Interface. In Workshop on User Interfaces for Theorem Provers, C. Kaliszyk and C. Lüth (Eds.), Cited by: p1.
  27. [16] M. Iancu and F. Rabe (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.
  28. [30] F. Rabe and K. Sojakova (2012) Mechanically Verifying Logic Translations. In Workshop on Algebraic Development Techniques, Cited by: p1.
  29. [34] F. Rabe (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.
  30. [3] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, F. Rabe, and K. Sojakova (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.
  31. [6] C. David, M. Kohlhase, C. Lange, F. Rabe, and V. Zholudev (2010-06) JOBAD/MMT – interactive mathematics. In AI Mashup ChallengeAI Mashup Challenge at ESWC, A. Giurca, B. Endres-Niggemeyer, C. Lange, L. Maicher, and P. Hitzler (Eds.), External Links: Link Cited by: p1.
  32. [5] C. David, M. Kohlhase, C. Lange, F. Rabe, N. Zhiltsov, and V. Zholudev (2010) Publishing math lecture notes as linked data. In The semantic web: research and applications (part II)The Semantic Web: Research and Applications (Part II), L. Aroyo, G. Antoniou, E. Hyvönen, A. ten Teije, H. Stuckenschmidt, L. Cabral, and T. Tudorache (Eds.), LNCS, pp. 370–375. External Links: 1004.3390v1 Cited by: p1.
  33. [7] C. David, C. Lange, and F. Rabe (2010) Interactive documents as interfaces to computer algebra systems: JOBAD and Wolfram—Alpha. In CALCULEMUS (emerging trends)CALCULEMUS (Emerging Trends), D. Delahaye and R. Rioboo (Eds.), pp. 13–30. External Links: Link Cited by: p1.
  34. [33] F. Rabe (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.
  35. [45] V. Zholudev, M. Kohlhase, and F. Rabe (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.
  36. [9] J. Gičeva, C. Lange, and F. Rabe (2009-07) Integrating web services into active mathematical documents. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI, pp. 279–293. External Links: Link Cited by: p1.
  37. [8] S. Dumbrava, F. Horozal, and K. Sojakova (2009) A Case Study on Formalizing Algebra in a Module System. In Workshop on Modules and Libraries for Proof Assistants, F. Rabe and C. Schürmann (Eds.), ACM International Conference Proceeding Series, Vol. 429, pp. 11–18. Cited by: p1.
  38. [10] F. Horozal and F. Rabe (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.
  39. [29] F. Rabe and C. Schürmann (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.
  40. [32] F. Rabe (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.
  41. [1] C. Benzmüller, F. Rabe, and G. Sutcliffe (2008) THF0 – The core of the TPTP Language for Higher-Order Logic. In 4th International Joint Conference on Automated Reasoning, A. Armando, P. Baumgartner, and G. Dowek (Eds.), LNCS, pp. 491–506. Cited by: p1.
  42. [21] C. Lange, S. McLaughlin, and F. Rabe (2008) Flyspeck in a semantic wiki – collaborating on a large scale formalization of the Kepler conjecture. In Proceedings of the 3rd workshop on semantic wikis, European Semantic Web Conference3rd Workshop on Semantic Wikis, C. Lange, S. Schaffert, H. Skaf-Molli, and M. Völkel (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  43. [25] F. Rabe and M. Kohlhase (2008) An exchange format for modular knowledge. In Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th 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.
  44. [26] F. Rabe and M. Kohlhase (2008) An Exchange Format for Modular Knowledge. In Proceedings of the LPAR Workshops on Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics, G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz (Eds.), CEUR Workshop Proceedings, Vol. 418, pp. 50–68. Cited by: p1.
  45. [31] F. Rabe (2007) OMDoc Theory Graphs Revisited. In Proceedings of the OpenMath/JEM workshop, Cited by: p1.

Technical Reports

  1. [7] T. Koprucki, M. Kohlhase, K. Tabelow, D. Müller, and F. Rabe (2017) Model pathway diagrams for the representation of mathematical models. WIAS Preprint Technical Report 2431. External Links: Document Cited by: p1.
  2. [8] S. L. Luca De Feo and T. Wiesing (2017) Support for the scscp interface protocol in all relevant components (sage, gap etc.) distribution. Deliverable Technical Report D3.3, OpenDreamKit. External Links: Link Cited by: p1.
  3. [1] P. Dehaye, M. Iancu, M. Kohlhase, A. Konovalov, S. Lelièvre, D. Müller, M. Pfeiffer, F. Rabe, N. M. Thiéry, and T. Wiesing (2016) Report on OpenDreamKit deliverable d6.3: design of triform (D/K/S) theories (specification/rnc schema/examples) and implementation of triform theories in the MMT API. Deliverable Technical Report D6.2, OpenDreamKit. External Links: Link Cited by: p1.
  4. [2] P. Dehaye, M. Iancu, M. Kohlhase, A. Konovalov, S. Lelièvre, D. Müller, M. Pfeiffer, F. Rabe, N. M. Thiéry, and T. Wiesing (2016) Report on OpenDreamKit deliverables d6.2: initial D/K/S base design (including base survey and requirements workshop report) and d6.3: design of triform (D/K/S) theories (specification/RNC schema/examples) and implementation of triform theories in the mmt api. Deliverable Technical Report D6.2, OpenDreamKit. External Links: Link Cited by: p1.
  5. [9] F. Rabe and M. Kohlhase (2012) An XML-based syntax for MMT. Technical report Cited by: p1.
  6. [3] M. Iancu, M. Kohlhase, and F. Rabe (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.
  7. [10] V. Zholudev, M. Kohlhase, and F. Rabe (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.
  8. [6] M. Kohlhase, C. Lange, C. Müller, N. Müller, and F. Rabe (2009-02) Notations for active mathematical documents. KWARC Report Technical Report 2009-1, Jacobs University Bremen. Note: https://kwarc.info/publications/papers/KLMMR_NfAD.pdf External Links: Link Cited by: p1.
  9. [4] M. Kohlhase, C. Lange, C. Müller, N. Müller, and F. Rabe (2009) Notations for Active Mathematical Documents. Technical report Technical Report 2009-1, Jacobs University Bremen. Cited by: p1.
  10. [5] M. Kohlhase, C. Lange, C. Müller, N. Müller, and F. Rabe (2008-04) Adaptation of notations in living mathematical documents. KWARC Report Technical Report 2008-2, Jacobs University Bremen. External Links: Link Cited by: p1.

Unpublished

  1. [15] N. Roux (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.
  2. [14] N. Roux (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. [6] F. Rabe and N. Roux (2021) Modular formalization of formal systems. Note: under review External Links: Link Cited by: p1.
  4. [13] N. Roux and F. Rabe (2021) Structure-Preserving Diagram Operators. In Recent Trends in Algebraic Development Techniques, M. Roggenbach (Ed.), Lecture Notes in Computer Science, Vol. 12669, pp. 142–163. External Links: Link, ISBN 978-3-030-73785-6, Document Cited by: 12.
  5. [11] N. Roux and F. Rabe (2020) Diagram Operators in a Logical Framework. Extended Abstract, Frontiers in Artificial Intelligence and Applications. External Links: Link Cited by: p1.
  6. [12] N. Roux and F. Rabe (2020) Functorial Diagram Operators. Extended Abstract. Note: Extended abstract accepted as [13] Cited by: p1.
  7. [5] F. Rabe and D. Müller (2018) Structuring theories with implicit morphisms. Extended Abstract. External Links: Link Cited by: p1.
  8. [10] F. Rabe (2018) MMT: a foundation-independent logical framework. Online Documentation. External Links: Link Cited by: p1.
  9. [2] M. Iancu, M. Kohlhase, F. Rabe, and H. Yuan (2016) Mixing surface languages for OMDoc. External Links: Link Cited by: p1.
  10. [3] M. Iancu, M. Kohlhase, and F. Rabe (2016) Understanding the pragmatics of module systems for mathematics. External Links: Link Cited by: p1.
  11. [9] F. Rabe (2012) A type theory based on reflection. Note: Manuscript Cited by: p1.
  12. [1] F. Horozal, M. Kohlhase, F. Rabe, and K. Sojakova (2010) Towards an atlas of logics. External Links: Link Cited by: p1.
  13. [4] F. Rabe and M. Iancu (2010) A Formalized Set-Theoretical Semantics of Isabelle/HOL. External Links: Link Cited by: p1.
  14. [8] F. Rabe (2009) The MMT Language. Cited by: p1.
  15. [7] F. Rabe (2008) Institutions with Proofs and their Representation in a Logical Framework. External Links: Link Cited by: p1.

Miscellaneous

  1. [8] V. Zamdzhiev (2011) Universal OpenMath machine. B. Sc. Thesis, Jacobs University Bremen. Cited by: p1.
  2. [1] S. Dumbrava and F. Rabe (2010) Structuring Theories with Partial Morphisms. Note: Workshop on Abstract Development Techniques Cited by: p1.
  3. [2] S. Dumbrava (2010) Structured specifications with hiding in the edinburgh logical framework LF. Bachelor’s Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  4. [3] F. Horozal and F. Rabe (2009) A Formal Proof of the Soundness of First-order Logic. Cited by: p1.
  5. [4] A. Iacob (2009) Reasoning about theory morphisms. Bachelor’s Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  6. [5] M. Kohlhase, T. Mossakowski, and F. Rabe (2009) The LATIN Project. External Links: Link Cited by: p1.
  7. [6] F. Rabe and C. Schürmann (2009) A Module System for Twelf. External Links: Link Cited by: p1.
  8. [7] F. Rabe The MMT language and system. External Links: Link Cited by: p1.