Project LATIN : 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. [2] 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.
  2. [3] F. Rabe and M. Kohlhase (2013) A scalable module system. Information & Computation 0 (230), pp. 1–54. External Links: Link Cited by: p1.
  3. [4] F. Rabe and K. Sojakova (2013) Logical Relations for a Logical Framework. ACM Transactions on Computational Logic. External Links: Link Cited by: p1.
  4. [1] 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.

Papers at International, Peer-Reviewed Conferences

  1. [8] 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.
  2. [6] 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.
  3. [7] 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.
  4. [11] 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.
  5. [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.
  6. [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.
  7. [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.
  8. [4] 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.
  9. [5] F. Horozal, M. Kohlhase, and F. Rabe (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.
  10. [9] 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.
  11. [10] 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.
  12. [13] 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.
  13. [12] 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.

Theses

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

Gray Literature

Papers at Peer-Reviewed Workshops

  1. [9] 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. [12] 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. [13] F. Rabe and N. Roux (2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style. In Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), E. Pimentel and E. Tassi (Eds.), pp. 88–103. Cited by: p1.
  4. [1] 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.
  5. [3] M. Codescu, F. Horozal, T. Mossakowski, and F. Rabe (2012) Compiling Logics. In Workshop on Algebraic Development Techniques, Cited by: p1.
  6. [6] 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.
  7. [7] 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.
  8. [15] F. Rabe and K. Sojakova (2012) Mechanically Verifying Logic Translations. In Workshop on Algebraic Development Techniques, Cited by: p1.
  9. [18] 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.
  10. [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.
  11. [5] F. Horozal, M. Kohlhase, and F. Rabe (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.
  12. [17] 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.
  13. [19] 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.
  14. [8] M. Kohlhase and F. Rabe (2009-07) Semantics of OpenMath and MathML3. In 22nd openmath workshop22nd OpenMath Workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1.
  15. [11] F. Rabe and M. Kohlhase (2009-07) A better role system for OpenMath. In 22nd openmath workshop22nd OpenMath Workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1.
  16. [4] 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.
  17. [14] 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.
  18. [16] 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.
  19. [10] 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.

Technical Reports

  1. [1] 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.
  2. [2] 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.

Unpublished

  1. [4] 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. [3] 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. [1] F. Horozal, M. Kohlhase, F. Rabe, and K. Sojakova (2010) Towards an atlas of logics. External Links: Link Cited by: p1.
  4. [2] F. Rabe and M. Iancu (2010) A Formalized Set-Theoretical Semantics of Isabelle/HOL. External Links: Link Cited by: p1.

Miscellaneous

  1. [1] F. Horozal and F. Rabe (2009) A Formal Proof of the Soundness of First-order Logic. Cited by: p1.
  2. [2] M. Kohlhase, T. Mossakowski, and F. Rabe (2009) The LATIN Project. External Links: Link Cited by: p1.
  3. [3] F. Rabe and C. Schürmann (2009) A Module System for Twelf. External Links: Link Cited by: p1.