Patents

1. Retaining Dafny Specifications, T. Xiang, S. McLaughlin, M. Rapoport, N. Runga, M. Schlaipfer, Florian Rabe, 2024
   United States Patent, No. US 11,921,616 B1
   BibTex@misc{AWS:dafny:24, author = "T. Xiang and S. McLaughlin and M. Rapoport and N. Runga and M. Schlaipfer and F. Rabe", title = "{Retaining Dafny Specifications}", year = "2024", note = "United States Patent, No. US 11,921,616 B1" }

Articles in Journals

1. Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401), A. Bauer, Katja Berčič, N. Thiéry, Florian Rabe, J. Taslak, 2024
   Dagstuhl Reports by Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 13(10):1-23
   BibTex@article{mathdagstuhl:23, author = "A. Bauer and K. Ber{\v{c}}i{\v{c}} and N. Thi{\'e}ry and F. Rabe and J. Taslak", title = "{Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401)}", year = "2024", pages = "1--23", journal = "Dagstuhl Reports by Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik", volume = "13", number = "10" }
2. Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge, J. Carette, W. Farmer, Michael Kohlhase, Florian Rabe, 2021
   The Mathematical Intelligencer, 43(1):78-87
   BibTex@article{CFKR:tetrapod:19, author = "J. Carette and W. Farmer and M. Kohlhase and F. Rabe", title = "{Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge}", year = "2021", pages = "78--87", journal = "The Mathematical Intelligencer", volume = "43", number = "1" }
3. Experiences from Exporting Major Proof Assistant Libraries, Michael Kohlhase, Florian Rabe, 2021
   Journal of Automated Reasoning, 65(8):1265-1298
   BibTex@article{KR:oafexp:20, author = "M. Kohlhase and F. Rabe", title = "{Experiences from Exporting Major Proof Assistant Libraries}", year = "2021", pages = "1265--1298", journal = "Journal of Automated Reasoning", volume = "65", number = "8" } Slides
4. (Deep) FAIR Mathematics, Katja Berčič, Michael Kohlhase, Florian Rabe, 2020
   it - Information Technology, 62(1):7-17
   BibTex@article{BKR:deepfair:20, author = "K. Ber{\v{c}}i{\v{c}} and M. Kohlhase and F. Rabe", title = "{(Deep) FAIR Mathematics}", year = "2020", pages = "7--17", journal = "it - Information Technology", volume = "62", number = "1" }
5. A Modular Type Reconstruction Algorithm, Florian Rabe, 2018
   ACM Transactions on Computational Logic, 19(4):1-43
   BibTex@article{rabe:recon:17, author = "F. Rabe", title = "{A Modular Type Reconstruction Algorithm}", year = "2018", pages = "1--43", journal = "ACM Transactions on Computational Logic", volume = "19", number = "4" }
6. Model pathway diagrams for the representation of mathematical models, T. Koprucki, Michael Kohlhase, K. Tabelow, Dennis Müller, Florian Rabe, 2018
   Optical and Quantum Electronics, 50(70)
   BibTex@article{KKTMR:mpd:17, author = "T. Koprucki and M. Kohlhase and K. Tabelow and D. M{\"u}ller and F. Rabe", title = "{Model pathway diagrams for the representation of mathematical models}", year = "2018", journal = "Optical and Quantum Electronics", volume = "50", number = "70" }
7. How to Identify, Translate, and Combine Logics?, Florian Rabe, 2017
   Journal of Logic and Computation, 27(6):1753-1798
   BibTex@article{rabe:howto:14, author = "F. Rabe", title = "{How to Identify, Translate, and Combine Logics?}", year = "2017", pages = "1753--1798", journal = "Journal of Logic and Computation", volume = "27", number = "6" }
8. Morphism Axioms, Florian Rabe, 2017
   Theoretical Computer Science, 691:55-80
   BibTex@article{rabe:maxioms:16, author = "F. Rabe", title = "{Morphism Axioms}", year = "2017", pages = "55--80", journal = "Theoretical Computer Science", volume = "691" }
9. Universality of Proofs (Dagstuhl Seminar 16421), G. Dowek, C. Dubois, B. Pientka, F. Rabe, 2017
   Dagstuhl Reports by Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 6(10):75-98
   BibTex@article{universality:16, author = "G. Dowek and C. Dubois and B. Pientka and F. Rabe", title = "{Universality of Proofs (Dagstuhl Seminar 16421)}", year = "2017", note = "see \url{http://drops.dagstuhl.de/opus/volltexte/2017/6951/}", pages = "75--98", journal = "Dagstuhl Reports by Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik", volume = "6", number = "10" }
10. QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge, Michael Kohlhase, Florian Rabe, 2016
    Journal of Formalized Reasoning, 9(1):201-234
    BibTex@article{KR:qed:14, author = "M. Kohlhase and F. Rabe", title = "{QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge}", year = "2016", pages = "201--234", journal = "Journal of Formalized Reasoning", volume = "9", number = "1" }
11. Lax Theory Morphisms, Florian Rabe, 2015
    ACM Transactions on Computational Logic, 17(1)
    BibTex@article{rabe:lax:14, author = "F. Rabe", title = "{Lax Theory Morphisms}", year = "2015", journal = "ACM Transactions on Computational Logic", volume = "17", number = "1" }
12. The Future of Logic: Foundation-Independence, Florian Rabe, 2015
    Logica Universalis, 10(1):1-20
    10.1007/s11787-015-0132-x; Winner of the Contest ``The Future of Logic'' at the World Congress on Universal Logic
    BibTex@article{rabe:future:15, author = "F. Rabe", title = "{The Future of Logic: Foundation-Independence}", year = "2015", note = "10.1007/s11787-015-0132-x; Winner of the Contest ``The Future of Logic'' at the World Congress on Universal Logic", pages = "1--20", journal = "Logica Universalis", volume = "10", number = "1" } Slides
13. A Logical Framework Combining Model and Proof Theory, Florian Rabe, 2013
    Mathematical Structures in Computer Science, 23(5):945-1001
    BibTex@article{rabe:combining:10, author = "F. Rabe", title = "{A Logical Framework Combining Model and Proof Theory}", year = "2013", pages = "945--1001", journal = "Mathematical Structures in Computer Science", volume = "23", number = "5" }
14. A Scalable Module System, Florian Rabe, Michael Kohlhase, 2013
    Information and Computation, 230(1):1-54
    BibTex@article{RK:mmt:10, author = "F. Rabe and M. Kohlhase", title = "{A Scalable Module System}", year = "2013", pages = "1--54", journal = "Information and Computation", volume = "230", number = "1" }
15. Logical Relations for a Logical Framework, Florian Rabe, Kristina Sojakova, 2013
    ACM Transactions on Computational Logic, 14(4):1-34
    BibTex@article{RS:logrels:12, author = "F. Rabe and K. Sojakova", title = "{Logical Relations for a Logical Framework}", year = "2013", pages = "1--34", journal = "ACM Transactions on Computational Logic", volume = "14", number = "4" }
16. The Mizar Mathematical Library in OMDoc: Translation and Applications, Mihnea Iancu, Michael Kohlhase, Florian Rabe, Josef Urban, 2013
    Journal of Automated Reasoning, 50(2):191-202
    BibTex@article{IKRU:mizar:11, author = "M. Iancu and M. Kohlhase and F. Rabe and J. Urban", title = "{The Mizar Mathematical Library in OMDoc: Translation and Applications}", year = "2013", pages = "191--202", journal = "Journal of Automated Reasoning", volume = "50", number = "2" }
17. Semantics of OpenMath and MathML3, Michael Kohlhase, Florian Rabe, 2012
    Mathematics in Computer Science, 6(3):235-260
    BibTex@article{KR:omsemantics:12, author = "M. Kohlhase and F. Rabe", title = "{Semantics of OpenMath and MathML3}", year = "2012", pages = "235--260", journal = "Mathematics in Computer Science", volume = "6", number = "3" }
18. Formalizing Foundations of Mathematics, Mihnea Iancu, Florian Rabe, 2011
    Mathematical Structures in Computer Science, 21(4):883-911
    BibTex@article{IR:foundations:10, author = "M. Iancu and F. Rabe", title = "{Formalizing Foundations of Mathematics}", year = "2011", pages = "883--911", journal = "Mathematical Structures in Computer Science", volume = "21", number = "4" }
19. Kripke Semantics for Martin-Löf's Extensional Type Theory, Steve Awodey, Florian Rabe, 2011
    Logical Methods in Computer Science, 7(3)
    BibTex@article{AR:lamkrip:11, author = "S. Awodey and F. Rabe", title = "{Kripke Semantics for Martin-L{\"o}f's Extensional Type Theory}", year = "2011", journal = "Logical Methods in Computer Science", volume = "7", number = "3" }
20. Representing Model Theory in a Type-Theoretical Logical Framework, Fulya Horozal, Florian Rabe, 2011
    Theoretical Computer Science, 412(37):4919-4945
    BibTex@article{HR:folsound:10, author = "F. Horozal and F. Rabe", title = "{Representing Model Theory in a Type-Theoretical Logical Framework}", year = "2011", pages = "4919--4945", journal = "Theoretical Computer Science", volume = "412", number = "37" }
21. An Institutional View on Categorical Logic, Joseph Goguen, Till Mossakowski, Valeria de Paiva, Florian Rabe, Lutz Schröder, 2007
    International Journal of Software and Informatics, 1(1):129-152
    BibTex@article{GMPRS:catlog:07, author = "J. Goguen and T. Mossakowski and V. {de Paiva} and F. Rabe and L. Schr{\"o}der", title = "{An Institutional View on Categorical Logic}", year = "2007", pages = "129--152", journal = "International Journal of Software and Informatics", volume = "1", number = "1" }
22. Solving the $100 Modal Logic Challenge, Florian Rabe, P. Pudlák, Geoff Sutcliffe, W. Shen, 2007
    Journal of Applied Logic, 7(1):113-130
    BibTex@article{RPSS:moloss:07, author = "F. Rabe and P. Pudl{\'a}k and G. Sutcliffe and W. Shen", title = "{Solving the \$100 Modal Logic Challenge}", year = "2007", pages = "113--130", journal = "Journal of Applied Logic", volume = "7", number = "1" }

Refereed Articles in Major Collections

1. A Logical Framework Perspective on Conservativity, Florian Rabe, 2024
   Intelligent Computer Mathematics, A. Kohlhase, L. Kovacs (eds.) , Lecture Notes in Computer Science, Springer
   BibTex@inproceedings{rabe:cons:24, author = "F. Rabe", title = "{A Logical Framework Perspective on Conservativity}", year = "2024", booktitle = "Intelligent Computer Mathematics", editor = "A. Kohlhase and L. Kovacs", publisher = "Springer" }
2. Extracting Theory Graphs from Aldor Libraries, Florian Rabe, S. Watt, 2023
   Intelligent Computer Mathematics, C. Dubois, M. Kerber (eds.), pp. 315-320 , volume 14101 of Lecture Notes in Computer Science, Springer
   BibTex@inproceedings{RW:aldor:23, author = "F. Rabe and S. Watt", title = "{Extracting Theory Graphs from Aldor Libraries}", year = "2023", pages = "315--320", booktitle = "Intelligent Computer Mathematics", editor = "C. Dubois and M. Kerber", publisher = "Springer" } Slides
3. Morphism Equality in Theory Graphs, Florian Rabe, Franzika Weber, 2023
   Intelligent Computer Mathematics, C. Dubois, M. Kerber (eds.), pp. 174-189 , volume 14101 of Lecture Notes in Computer Science, Springer
   BibTex@inproceedings{RW:morpheq:23, author = "F. Rabe and F. Weber", title = "{Morphism Equality in Theory Graphs}", year = "2023", pages = "174--189", booktitle = "Intelligent Computer Mathematics", editor = "C. Dubois and M. Kerber", publisher = "Springer" } Slides
4. Theorem Proving in Dependently Typed Higher-Order Logic, Colin Rothgang, Florian Rabe, C. Benzmüller, 2023
   Automated Dedution, B. Pientka, C. Tinelli (eds.), pp. 438-455 , volume 14132 of Lecture Notes in Computer Science, Springer
   BibTex@inproceedings{RRB:dhol:23, author = "C. Rothgang and F. Rabe and C. Benzmüller", title = "{Theorem Proving in Dependently Typed Higher-Order Logic}", year = "2023", pages = "438--455", booktitle = "Automated Dedution", editor = "B. Pientka and C. Tinelli", publisher = "Springer" }
5. A Language with Type-Dependent Equality, Florian Rabe, 2021
   Intelligent Computer Mathematics, F. Kamareddine, C. Sacerdoti Coen (eds.), pp. 211-227 , volume 12833 of Lecture Notes in Computer Science, Springer
   BibTex@inproceedings{rabe:tde:21, author = "F. Rabe", title = "{A Language with Type-Dependent Equality}", year = "2021", pages = "211--227", booktitle = "Intelligent Computer Mathematics", editor = "F. Kamareddine and C. {Sacerdoti Coen}", publisher = "Springer" } Slides
6. A New Export of the Mizar Mathematical Library, Colin Rothgang, A. Kornilowicz, Florian Rabe, 2021
   Intelligent Computer Mathematics, F. Kamareddine, C. Sacerdoti Coen (eds.), pp. 205-210 , volume 12833 of Lecture Notes in Computer Science, Springer
   BibTex@inproceedings{RKR:mizar:21, author = "C. Rothgang and A. Kornilowicz and F. Rabe", title = "{A New Export of the Mizar Mathematical Library}", year = "2021", pages = "205--210", booktitle = "Intelligent Computer Mathematics", editor = "F. Kamareddine and C. {Sacerdoti Coen}", publisher = "Springer" }
7. 3-Dimensional Graph Visualization of Mathematical Knowledge, Richard Marcus, Michael Kohlhase, Florian Rabe, 2020
   Intelligent Computer Mathematics, C. Benzmüller, B. Miller (eds.), pp. 290-296 , volume 12236 of Lecture Notes in Computer Science, Springer
   BibTex@inproceedings{MKR:tgview3d:20, author = "R. Marcus and M. Kohlhase and F. Rabe", title = "{3-Dimensional Graph Visualization of Mathematical Knowledge}", year = "2020", pages = "290--296", booktitle = "Intelligent Computer Mathematics", editor = "C. Benzmüller and B. Miller", publisher = "Springer" }
8. A Survey of Languages for Formalizing Mathematics, Cezary Kaliszyk, Florian Rabe, 2020
   Intelligent Computer Mathematics, C. Benzmüller, B. Miller (eds.), pp. 138-156 , volume 12236 of Lecture Notes in Computer Science, Springer
   BibTex@inproceedings{KR:ilfsurvey:20, author = "C. Kaliszyk and F. Rabe", title = "{A Survey of Languages for Formalizing Mathematics}", year = "2020", pages = "138--156", booktitle = "Intelligent Computer Mathematics", editor = "C. Benzmüller and B. Miller", publisher = "Springer" }
9. Logic-Independent Proof Search in Logical Frameworks (short paper), Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer, 2020
   Automated Reasoning, N. Peltier, V. Sofronie-Stokkermans (eds.), pp. 395-401 , volume 12166 of Lecture Notes in Computer Science, Springer
   BibTex@inproceedings{KRSS:mmtelpi:20, author = "M. Kohlhase and F. Rabe and C. {Sacerdoti Coen} and J. Schaefer", title = "{Logic-Independent Proof Search in Logical Frameworks (short paper)}", year = "2020", pages = "395--401", booktitle = "Automated Reasoning", editor = "N. Peltier and V. Sofronie-Stokkermans", publisher = "Springer" }
10. Representing Structural Language Features in Formal Meta-Languages, Dennis Müller, Colin Rothgang, Florian Rabe, Michael Kohlhase, 2020
    Intelligent Computer Mathematics, C. Benzmüller, B. Miller (eds.), pp. 206-221 , volume 12236 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{MRRK:strucfeat:20, author = "D. M{\"u}ller and C. Rothgang and F. Rabe and M. Kohlhase", title = "{Representing Structural Language Features in Formal Meta-Languages}", year = "2020", pages = "206--221", booktitle = "Intelligent Computer Mathematics", editor = "C. Benzmüller and B. Miller", publisher = "Springer" }
11. Structure-Preserving Diagram Operators, Florian Rabe, Navid Roux, 2020
    Recent Trends in Algebraic Development Techniques, M. Roggenbach (eds.), pp. 142-163 , volume 12669 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{RR:linearops:20, author = "F. Rabe and N. Roux", title = "{Structure-Preserving Diagram Operators}", year = "2020", pages = "142--163", booktitle = "Recent Trends in Algebraic Development Techniques", editor = "M. Roggenbach", publisher = "Springer" }
12. Towards a Heterogeneous Query Language for Mathematical Knowledge, Katja Berčič, Michael Kohlhase, Florian Rabe, 2020
    Intelligent Computer Mathematics, C. Benzmüller, B. Miller (eds.), pp. 39-54 , volume 12236 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{BKR:mdql:20, author = "K. Ber{\v{c}}i{\v{c}} and M. Kohlhase and F. Rabe", title = "{Towards a Heterogeneous Query Language for Mathematical Knowledge}", year = "2020", pages = "39--54", booktitle = "Intelligent Computer Mathematics", editor = "C. Benzmüller and B. Miller", publisher = "Springer" } Slides
13. Diagram Operators in MMT, Y. Sharoda, Florian Rabe, 2019
    Intelligent Computer Mathematics, C. Kaliszyk, E. Brady, A. Kohlhase, C. Sacerdoti Coen (eds.), pp. 211-226 , volume 11617 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{RS:diagops:19, author = "Y. Sharoda and F. Rabe", title = "{Diagram Operators in MMT}", year = "2019", pages = "211--226", booktitle = "Intelligent Computer Mathematics", editor = "C. Kaliszyk and E. Brady and A. Kohlhase and C. {Sacerdoti Coen}", publisher = "Springer" }
14. How to calculate with nondeterministic functions, R. Bird, Florian Rabe, 2019
    Mathematics of Program Construction, G. Hutton (eds.), pp. 138-154 , volume 11825 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{BR:nondet:19, author = "R. Bird and F. Rabe", title = "{How to calculate with nondeterministic functions}", year = "2019", pages = "138--154", booktitle = "Mathematics of Program Construction", editor = "G. Hutton", publisher = "Springer" } Slides
15. Integrating Semantic Mathematical Documents and Dynamic Notebooks, Kai Amann, Michael Kohlhase, Florian Rabe, Tom Wiesing, 2019
    Intelligent Computer Mathematics, C. Kaliszyk, E. Brady, A. Kohlhase, C. Sacerdoti Coen (eds.), pp. 275-290 , volume 11617 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{AKRW:jupyter:19, author = "K. Amann and M. Kohlhase and F. Rabe and T. Wiesing", title = "{Integrating Semantic Mathematical Documents and Dynamic Notebooks}", year = "2019", pages = "275--290", booktitle = "Intelligent Computer Mathematics", editor = "C. Kaliszyk and E. Brady and A. Kohlhase and C. {Sacerdoti Coen}", publisher = "Springer" }
16. Making Isabelle Content Accessible in Knowledge Representation Formats, Michael Kohlhase, Florian Rabe, M. Wenzel, 2019
    Types for Proofs and Programs (TYPES), M. Bezem, A. Mahboubi (eds.) , volume 175 of LIPIcs---Leibniz International Proceedings in Informatics, Schloss Dagstuhl--–Leibniz Center for Informatics
    BibTex@inproceedings{KRW:isabelle:19, author = "M. Kohlhase and F. Rabe and M. Wenzel", title = "{Making Isabelle Content Accessible in Knowledge Representation Formats}", year = "2019", booktitle = "Types for Proofs and Programs (TYPES)", editor = "M. Bezem and A. Mahboubi", publisher = "Schloss Dagstuhl--–Leibniz Center for Informatics" }
17. MMTTeX: Connecting Content and Narration-Oriented Document Formats, Florian Rabe, 2019
    Intelligent Computer Mathematics, C. Kaliszyk, E. Brady, A. Kohlhase, C. Sacerdoti Coen (eds.), pp. 205-210 , volume 11617 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{rabe:mmttex:19, author = "F. Rabe", title = "{MMTTeX: Connecting Content and Narration-Oriented Document Formats}", year = "2019", pages = "205--210", booktitle = "Intelligent Computer Mathematics", editor = "C. Kaliszyk and E. Brady and A. Kohlhase and C. {Sacerdoti Coen}", publisher = "Springer" } Slides
18. Relational Data Across Mathematical Libraries, A. Condoluci, Michael Kohlhase, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen, M. Wenzel, 2019
    Intelligent Computer Mathematics, C. Kaliszyk, E. Brady, A. Kohlhase, C. Sacerdoti Coen (eds.), pp. 61-76 , volume 11617 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{CKMRSW:ulo:19, author = "A. Condoluci and M. Kohlhase and D. M{\"u}ller and F. Rabe and C. {Sacerdoti Coen} and M. Wenzel", title = "{Relational Data Across Mathematical Libraries}", year = "2019", pages = "61--76", booktitle = "Intelligent Computer Mathematics", editor = "C. Kaliszyk and E. Brady and A. Kohlhase and C. {Sacerdoti Coen}", publisher = "Springer" }
19. Structuring Theories with Implicit Morphisms, Dennis Müller, Florian Rabe, 2019
    Recent Trends in Algebraic Development Techniques, J. Fiadeiro, I. Tutu (eds.), pp. 154-173 , volume 11563 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{MR:implicit:19, author = "D. M{\"u}ller and F. Rabe", title = "{Structuring Theories with Implicit Morphisms}", year = "2019", pages = "154--173", booktitle = "Recent Trends in Algebraic Development Techniques", editor = "J. Fiadeiro and I. Tutu", publisher = "Springer" }
20. The Coq Library as a Theory Graph, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen, 2019
    Intelligent Computer Mathematics, C. Kaliszyk, E. Brady, A. Kohlhase, C. Sacerdoti Coen (eds.), pp. 171-186 , volume 11617 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{MRS:coq:19, author = "D. M{\"u}ller and F. Rabe and C. {Sacerdoti Coen}", title = "{The Coq Library as a Theory Graph}", year = "2019", pages = "171--186", booktitle = "Intelligent Computer Mathematics", editor = "C. Kaliszyk and E. Brady and A. Kohlhase and C. {Sacerdoti Coen}", publisher = "Springer" }
21. Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation, Katja Berčič, Michael Kohlhase, Florian Rabe, 2019
    Intelligent Computer Mathematics, C. Kaliszyk, E. Brady, A. Kohlhase, C. Sacerdoti Coen (eds.), pp. 28-43 , volume 11617 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{BKR:data:19, author = "K. Ber{\v{c}}i{\v{c}} and M. Kohlhase and F. Rabe", title = "{Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation}", year = "2019", pages = "28--43", booktitle = "Intelligent Computer Mathematics", editor = "C. Kaliszyk and E. Brady and A. Kohlhase and C. {Sacerdoti Coen}", publisher = "Springer" }
22. Automatically Finding Theory Morphisms for Knowledge Management, Dennis Müller, Michael Kohlhase, Florian Rabe, 2018
    Intelligent Computer Mathematics, F. Rabe, W. Farmer, G. Passmore, A. Youssef (eds.), pp. 209-224 , volume 11006 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{MKR:viewfinder:18, author = "D. M{\"u}ller and M. Kohlhase and F. Rabe", title = "{Automatically Finding Theory Morphisms for Knowledge Management}", year = "2018", pages = "209--224", booktitle = "Intelligent Computer Mathematics", editor = "F. Rabe and W. Farmer and G. Passmore and A. Youssef", publisher = "Springer" }
23. Theories as Types, Dennis Müller, Florian Rabe, Michael Kohlhase, 2018
    Automated Reasoning, D. Galmiche, S. Schulz, R. Sebastiani (eds.), pp. 575-590 , volume 10900 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{MRK:modelsof:18, author = "D. M{\"u}ller and F. Rabe and M. Kohlhase", title = "{Theories as Types}", year = "2018", pages = "575--590", booktitle = "Automated Reasoning", editor = "D. Galmiche and S. Schulz and R. Sebastiani", publisher = "Springer" }
24. Canonical Selection of Colimits, Mihai Codescu, Till Mossakowski, Florian Rabe, 2017
    Recent Trends in Algebraic Development Techniques, P. James, M. Roggenbach (eds.), pp. 170-188 , volume 10644 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{CMR:colimits:16, author = "M. Codescu and T. Mossakowski and F. Rabe", title = "{Canonical Selection of Colimits}", year = "2017", pages = "170--188", booktitle = "Recent Trends in Algebraic Development Techniques", editor = "P. James and M. Roggenbach", publisher = "Springer" }
25. Classification of Alignments between Concepts of Formal Mathematical Systems, Dennis Müller, T. Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe, 2017
    Intelligent Computer Mathematics, H. Geuvers, M. England, O. Hasan, F. Rabe, O. Teschke (eds.), pp. 83-98 , volume 10383 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{GKKMR:alignments:17, author = "D. M{\"u}ller and T. Gauthier and C. Kaliszyk and M. Kohlhase and F. Rabe", title = "{Classification of Alignments between Concepts of Formal Mathematical Systems}", year = "2017", pages = "83--98", booktitle = "Intelligent Computer Mathematics", editor = "H. Geuvers and M. England and O. Hasan and F. Rabe and O. Teschke", publisher = "Springer" }
26. Knowledge-Based Interoperability for Mathematical Software Systems, Michael Kohlhase, Dennis Müller, M. Pfeiffer, Florian Rabe, N. Thiéry, V. Vasilyev, T. Wiesing, 2017
    Mathematical Aspects of Computer and Information Sciences, J. Blömer, I. Kotsireas, T. Kutsia, D. Simos (eds.), pp. 195-210 , volume 10693 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{ODK:interop:17, author = "M. Kohlhase and D. M{\"u}ller and M. Pfeiffer and F. Rabe and N. Thi{\'e}ry and V. Vasilyev and T. Wiesing", title = "{Knowledge-Based Interoperability for Mathematical Software Systems}", year = "2017", pages = "195--210", booktitle = "Mathematical Aspects of Computer and Information Sciences", editor = "J. Bl{\"o}mer and I. Kotsireas and T. Kutsia and D. Simos", publisher = "Springer" }
27. Making PVS Accessible to Generic Services by Interpretation in a Universal Format, Michael Kohlhase, Dennis Müller, S. Owre, Florian Rabe, 2017
    Interactive Theorem Proving, M. Ayala-Rincon, C. Munoz (eds.), pp. 319-335 , volume 10499 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{KMOR:pvs:17, author = "M. Kohlhase and D. M{\"u}ller and S. Owre and F. Rabe", title = "{Making PVS Accessible to Generic Services by Interpretation in a Universal Format}", year = "2017", pages = "319--335", booktitle = "Interactive Theorem Proving", editor = "M. Ayala-Rincon and C. Munoz", publisher = "Springer" }
28. Virtual Theories -- A Uniform Interface to Mathematical Knowledge Bases, T. Wiesing, Michael Kohlhase, Florian Rabe, 2017
    Mathematical Aspects of Computer and Information Sciences, J. Blömer, I. Kotsireas, T. Kutsia, D. Simos (eds.), pp. 243-257 , volume 10693 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{WKR:virtual:17, author = "T. Wiesing and M. Kohlhase and F. Rabe", title = "{Virtual Theories -- A Uniform Interface to Mathematical Knowledge Bases}", year = "2017", pages = "243--257", booktitle = "Mathematical Aspects of Computer and Information Sciences", editor = "J. Bl{\"o}mer and I. Kotsireas and T. Kutsia and D. Simos", publisher = "Springer" }
29. Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach, P. Dehaye, Mihnea Iancu, Michael Kohlhase, A. Konovalov, S. Lelièvre, Dennis Müller, M. Pfeiffer, Florian Rabe, N. Thiéry, Tom Wiesing, 2016
    Intelligent Computer Mathematics, Michael Kohlhase, L. de Moura, M. Johansson, B. Miller, F. Tompa (eds.), pp. 117-131 , volume 9791 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{ODK:mitm:16, author = "P. Dehaye and M. Iancu and M. Kohlhase and A. Konovalov and S. Leli{\`e}vre and D. M{\"u}ller and M. Pfeiffer and F. Rabe and N. Thi{\'e}ry and T. Wiesing", title = "{Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach}", year = "2016", pages = "117--131", booktitle = "Intelligent Computer Mathematics", editor = "M. Kohlhase and L. {de Moura} and M. Johansson and B. Miller and F. Tompa", publisher = "Springer" }
30. Formal Logic Definitions for Interchange Languages, Fulya Horozal, Florian Rabe, 2015
    Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, Florian Rabe, V. Sorge (eds.), pp. 171-186 , volume 9150 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{HR:tptp:12, author = "F. Horozal and F. Rabe", title = "{Formal Logic Definitions for Interchange Languages}", year = "2015", pages = "171--186", booktitle = "Intelligent Computer Mathematics", editor = "M. Kerber and J. Carette and C. Kaliszyk and F. Rabe and V. Sorge", publisher = "Springer" } Slides
31. Generic Literals, Florian Rabe, 2015
    Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, Florian Rabe, V. Sorge (eds.), pp. 102-117 , volume 9150 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{rabe:literals:14, author = "F. Rabe", title = "{Generic Literals}", year = "2015", pages = "102--117", booktitle = "Intelligent Computer Mathematics", editor = "M. Kerber and J. Carette and C. Kaliszyk and F. Rabe and V. Sorge", publisher = "Springer" } Slides
32. Flexary Operators for Formalized Mathematics, Fulya Horozal, Florian Rabe, Michael Kohlhase, 2014
    Intelligent Computer Mathematics, S. Watt, J. Davenport, A. Sexton, P. Sojka, J. Urban (eds.), pp. 312-327 , volume 8543 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{HRK:sequences:14, author = "F. Horozal and F. Rabe and M. Kohlhase", title = "{Flexary Operators for Formalized Mathematics}", year = "2014", pages = "312--327", booktitle = "Intelligent Computer Mathematics", editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban", publisher = "Springer" } Slides
33. Towards Knowledge Management for HOL Light, C. Kaliszyk, Florian Rabe, 2014
    Intelligent Computer Mathematics, S. Watt, J. Davenport, A. Sexton, P. Sojka, J. Urban (eds.), pp. 357-372 , volume 8543 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{KR:hollight:14, author = "C. Kaliszyk and F. Rabe", title = "{Towards Knowledge Management for HOL Light}", year = "2014", pages = "357--372", booktitle = "Intelligent Computer Mathematics", editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban", publisher = "Springer" } Slides
34. A Universal Machine for Biform Theory Graphs, Michael Kohlhase, Felix Mance, Florian Rabe, 2013
    Intelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, W. Windsteiger (eds.), pp. 82-97 , volume 7961 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{KMR:uom:13, author = "M. Kohlhase and F. Mance and F. Rabe", title = "{A Universal Machine for Biform Theory Graphs}", year = "2013", pages = "82--97", booktitle = "Intelligent Computer Mathematics", editor = "J. Carette and D. Aspinall and C. Lange and P. Sojka and W. Windsteiger", publisher = "Springer" } Slides
35. Compiling Logics, Mihai Codescu, Fulya Horozal, Aivaras Jakubauskas, Till Mossakowski, Florian Rabe, 2013
    Recent Trends in Algebraic Development Techniques 2012, N. Martí-Oliet, M. Palomino (eds.), pp. 111-126 , volume 7841 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{CHJMR:compiling:12, author = "M. Codescu and F. Horozal and A. Jakubauskas and T. Mossakowski and F. Rabe", title = "{Compiling Logics}", year = "2013", pages = "111--126", booktitle = "Recent Trends in Algebraic Development Techniques 2012", editor = "N. Mart{\'i}-Oliet and M. Palomino", publisher = "Springer" }
36. The MMT API: A Generic MKM System, Florian Rabe, 2013
    Intelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, W. Windsteiger (eds.), pp. 339-343 , volume 7961 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{rabe:mmtabs:13, author = "F. Rabe", title = "{The MMT API: A Generic MKM System}", year = "2013", pages = "339--343", booktitle = "Intelligent Computer Mathematics", editor = "J. Carette and D. Aspinall and C. Lange and P. Sojka and W. Windsteiger", publisher = "Springer" } Slides
37. A Proof Theoretic Interpretation of Model Theoretic Hiding, Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe, 2012
    Recent Trends in Algebraic Development Techniques 2010, Till Mossakowski, H. Kreowski (eds.), pp. 118-138 , volume 7137 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{CHKMR:hiding:11, author = "M. Codescu and F. Horozal and M. Kohlhase and T. Mossakowski and F. Rabe", title = "{A Proof Theoretic Interpretation of Model Theoretic Hiding}", year = "2012", pages = "118--138", booktitle = "Recent Trends in Algebraic Development Techniques 2010", editor = "T. Mossakowski and H. Kreowski", publisher = "Springer" }
38. A Query Language for Formal Mathematical Libraries, Florian Rabe, 2012
    Intelligent Computer Mathematics, J. Campbell, J. Carette, G. Dos Reis, J. Jeuring, P. Sojka, V. Sorge, M. Wenzel (eds.), pp. 142-157 , volume 7362 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{rabe:querying:12, author = "F. Rabe", title = "{A Query Language for Formal Mathematical Libraries}", year = "2012", pages = "142--157", booktitle = "Intelligent Computer Mathematics", editor = "J. Campbell and J. Carette and G. {Dos Reis} and J. Jeuring and P. Sojka and V. Sorge and M. Wenzel", publisher = "Springer" } Slides
39. Extending MKM Formats at the Statement Level, Fulya Horozal, Michael Kohlhase, Florian Rabe, 2012
    Intelligent Computer Mathematics, J. Campbell, J. Carette, G. Dos Reis, J. Jeuring, P. Sojka, V. Sorge, M. Wenzel (eds.), pp. 64-79 , volume 7362 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{HKR:extending:12, author = "F. Horozal and M. Kohlhase and F. Rabe", title = "{Extending MKM Formats at the Statement Level}", year = "2012", pages = "64--79", booktitle = "Intelligent Computer Mathematics", editor = "J. Campbell and J. Carette and G. {Dos Reis} and J. Jeuring and P. Sojka and V. Sorge and M. Wenzel", publisher = "Springer" }
40. Management of Change in Declarative Languages, Mihnea Iancu, Florian Rabe, 2012
    Intelligent Computer Mathematics, J. Campbell, J. Carette, G. Dos Reis, J. Jeuring, P. Sojka, V. Sorge, M. Wenzel (eds.), pp. 325-340 , volume 7362 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{IR:moc:12, author = "M. Iancu and F. Rabe", title = "{Management of Change in Declarative Languages}", year = "2012", pages = "325--340", booktitle = "Intelligent Computer Mathematics", editor = "J. Campbell and J. Carette and G. {Dos Reis} and J. Jeuring and P. Sojka and V. Sorge and M. Wenzel", publisher = "Springer" }
41. Towards Logical Frameworks in the Heterogeneous Tool Set Hets, Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe, Kristina Sojakova, 2012
    Recent Trends in Algebraic Development Techniques 2010, Till Mossakowski, H. Kreowski (eds.), pp. 139-159 , volume 7137 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{CHKMRS:lfhets:11, author = "M. Codescu and F. Horozal and M. Kohlhase and T. Mossakowski and F. Rabe and K. Sojakova", title = "{Towards Logical Frameworks in the Heterogeneous Tool Set Hets}", year = "2012", pages = "139--159", booktitle = "Recent Trends in Algebraic Development Techniques 2010", editor = "T. Mossakowski and H. Kreowski", publisher = "Springer" }
42. A Foundational View on Integration Problems, Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen, 2011
    Intelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, J. Urban (eds.), pp. 107-122 , volume 6824 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{RKS:integration:11, author = "F. Rabe and M. Kohlhase and C. {Sacerdoti Coen}", title = "{A Foundational View on Integration Problems}", year = "2011", pages = "107--122", booktitle = "Intelligent Computer Mathematics", editor = "J. Davenport and W. Farmer and F. Rabe and J. Urban", publisher = "Springer" } Slides
43. Combining Source, Content, Presentation, Narration, and Relational Representation, Fulya Horozal, Alin Iacob, Constantin Jucovschi, Michael Kohlhase, Florian Rabe, 2011
    Intelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, J. Urban (eds.), pp. 212-227 , volume 6824 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{HIJKR:dimensions:11, author = "F. Horozal and A. Iacob and C. Jucovschi and M. Kohlhase and F. Rabe", title = "{Combining Source, Content, Presentation, Narration, and Relational Representation}", year = "2011", pages = "212--227", booktitle = "Intelligent Computer Mathematics", editor = "J. Davenport and W. Farmer and F. Rabe and J. Urban", publisher = "Springer" }
44. Project Abstract: Logic Atlas and Integrator (LATIN), Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe, 2011
    Intelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, J. Urban (eds.), pp. 289-291 , volume 6824 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{CHKMR:latinabs:11, author = "M. Codescu and F. Horozal and M. Kohlhase and T. Mossakowski and F. Rabe", title = "{Project Abstract: Logic Atlas and Integrator (LATIN)}", year = "2011", pages = "289--291", booktitle = "Intelligent Computer Mathematics", editor = "J. Davenport and W. Farmer and F. Rabe and J. Urban", publisher = "Springer" } Slides
45. A [insert XML Format] Database for [insert cool application], Vyacheslav Zholudev, Michael Kohlhase, Florian Rabe, 2010
    XMLPrague 2010 , Proceedings of XMLPrague, XMLPrague.cz
    BibTex@inproceedings{ZKR:tntbase:10, author = "V. Zholudev and M. Kohlhase and F. Rabe", title = "{A [insert XML Format] Database for [insert cool application]}", year = "2010", booktitle = "XMLPrague 2010", publisher = "XMLPrague.cz" }
46. Publishing Math Lecture Notes as Linked Data, Catalin David, Michael Kohlhase, Christoph Lange, Florian Rabe, Vyacheslav Zholudev, 2010
    The Semantic Web: Research and Applications, L. Aroyo, G. Antoniou, E. Hyvönen, A. ten Teije, H. Stuckenschmidt, L. Cabral, T. Tudorache (eds.), pp. 370-375 , volume 6089 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{DKLRZ:jobaddemo:10, author = "C. David and M. Kohlhase and C. Lange and F. Rabe and V. Zholudev", title = "{Publishing Math Lecture Notes as Linked Data}", year = "2010", pages = "370--375", booktitle = "The Semantic Web: Research and Applications", editor = "L. Aroyo and G. Antoniou and E. Hyv{\"o}nen and A. {ten Teije} and H. Stuckenschmidt and L. Cabral and T. Tudorache", publisher = "Springer" }
47. Towards MKM in the Large: Modular Representation and Scalable Software Architecture, Michael Kohlhase, Florian Rabe, Vyacheslav Zholudev, 2010
    Intelligent Computer Mathematics, S. Autexier, J. Calmet, D. Delahaye, P. Ion, L. Rideau, R. Rioboo, A. Sexton (eds.), pp. 370-384 , volume 6167 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{KRZ:mmttnt:10, author = "M. Kohlhase and F. Rabe and V. Zholudev", title = "{Towards MKM in the Large: Modular Representation and Scalable Software Architecture}", year = "2010", pages = "370--384", booktitle = "Intelligent Computer Mathematics", editor = "S. Autexier and J. Calmet and D. Delahaye and P. Ion and L. Rideau and R. Rioboo and A. Sexton", publisher = "Springer" } Slides
48. Integrating Web Services into Active Mathematical Documents, Jana Gičeva, Christoph Lange, Florian Rabe, 2009
    Intelligent Computer Mathematics, J. Carette, L. Dixon, C. Sacerdoti Coen, S. Watt (eds.), pp. 279-293 , volume 5625 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{GLR:jobad:09, author = "J. Gi{\v{c}}eva and C. Lange and F. Rabe", title = "{Integrating Web Services into Active Mathematical Documents}", year = "2009", pages = "279--293", booktitle = "Intelligent Computer Mathematics", editor = "J. Carette and L. Dixon and C. {Sacerdoti Coen} and S. Watt", publisher = "Springer" }
49. Kripke Semantics for Martin-Löf's Extensional Type Theory, Steve Awodey, Florian Rabe, 2009
    Typed Lambda Calculi and Applications (TLCA), P. Curien (eds.), pp. 249-263 , volume 5608 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{AR:lamkrip:09, author = "S. Awodey and F. Rabe", title = "{Kripke Semantics for Martin-L{\"o}f's Extensional Type Theory}", year = "2009", pages = "249--263", booktitle = "Typed Lambda Calculi and Applications (TLCA)", editor = "P. Curien", publisher = "Springer" }
50. Translating a Dependently-Typed Logic to First-Order Logic, Kristina Sojakova, Florian Rabe, 2009
    Recent Trends in Algebraic Development Techniques, A. Corradini, U. Montanari (eds.), pp. 326-341 , volume 5486 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{SR:dfol_fol:08, author = "K. Sojakova and F. Rabe", title = "{Translating a Dependently-Typed Logic to First-Order Logic}", year = "2009", pages = "326--341", booktitle = "Recent Trends in Algebraic Development Techniques", editor = "A. Corradini and U. Montanari", publisher = "Springer" }
51. Notations for Living Mathematical Documents, Michael Kohlhase, Christine Müller, Florian Rabe, 2008
    Mathematical Knowledge Management, S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. Suzuki, F. Wiedijk (eds.), pp. 504-519 , volume 5144 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{KMR:presentation:08, author = "M. Kohlhase and C. M{\"u}ller and F. Rabe", title = "{Notations for Living Mathematical Documents}", year = "2008", pages = "504--519", booktitle = "Mathematical Knowledge Management", editor = "S. Autexier and J. Campbell and J. Rubio and V. Sorge and M. Suzuki and F. Wiedijk", publisher = "Springer" }
52. THF0 -- The core of the TPTP Language for Higher-Order Logic, Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe, 2008
    4th International Joint Conference on Automated Reasoning, A. Armando, P. Baumgartner, G. Dowek (eds.), pp. 491-506 , volume 5195 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{BRS:tptphol:08, author = "C. Benzm{\"u}ller and F. Rabe and G. Sutcliffe", title = "{THF0 -- The core of the TPTP Language for Higher-Order Logic}", year = "2008", pages = "491--506", booktitle = "4th International Joint Conference on Automated Reasoning", editor = "A. Armando and P. Baumgartner and G. Dowek", publisher = "Springer" }
53. First-Order Logic with Dependent Types, Florian Rabe, 2006
    Automated Reasoning, N. Shankar, U. Furbach (eds.), pp. 377-391 , volume 4130 of Lecture Notes in Computer Science, Springer
    BibTex@inproceedings{rabe:dfol:06, author = "F. Rabe", title = "{First-Order Logic with Dependent Types}", year = "2006", pages = "377--391", booktitle = "Automated Reasoning", editor = "N. Shankar and U. Furbach", publisher = "Springer" }

Under Review

Refereed Articles in Other Collections

1. Enhancing Proof Stability, S. McLaughlin, G. Jaloyan, T. Xiang, Florian Rabe, 2023
   Dafny 2024, J. Tassarotti, S. Zetzsche (eds.)
   BibTex@inproceedings{MJXR:dafnystability:23, author = "S. McLaughlin and G. Jaloyan and T. Xiang and F. Rabe", title = "{Enhancing Proof Stability}", year = "2023", booktitle = "Dafny 2024", editor = "J. Tassarotti and S. Zetzsche" }
2. The Potential of Answer Classes in Large-scale Written Computer Science Exams, D. Lohr, M. Berges, Michael Kohlhase, Florian Rabe, 2023
   Hochschuldidaktik Informatik (HDI), J. Desel, S. Opel (eds.)
   BibTex@inproceedings{LBKR:answerclasses:23, author = "D. Lohr and M. Berges and M. Kohlhase and F. Rabe", title = "{The Potential of Answer Classes in Large-scale Written Computer Science Exams}", year = "2023", booktitle = "Hochschuldidaktik Informatik (HDI)", editor = "J. Desel and S. Opel" }
3. Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style, Florian Rabe, Navid Roux, 2021
   Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), E. Pimentel, E. Tassi (eds.), pp. 88-103 , volume 337 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association
   BibTex@inproceedings{RR:soften:21, author = "F. Rabe and N. Roux", title = "{Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style}", year = "2021", pages = "88--103", booktitle = "Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP)", editor = "E. Pimentel and E. Tassi", publisher = "Open Publishing Association" }
4. Rapid Prototyping Formal Systems in MMT: Case Studies, Dennis Müller, Florian Rabe, 2019
   Logical Frameworks and Meta-languages: Theory and Practice, D. Miller, I. Scagnetto (eds.), pp. 40-54
   BibTex@inproceedings{MR:prototyping:19, author = "D. M{\"u}ller and F. Rabe", title = "{Rapid Prototyping Formal Systems in MMT: Case Studies}", year = "2019", pages = "40--54", booktitle = "Logical Frameworks and Meta-languages: Theory and Practice", editor = "D. Miller and I. Scagnetto" }
5. Alignment-based Translations Across Formal Systems Using Interface Theories, Dennis Müller, Colin Rothgang, Yufei Liu, Florian Rabe, 2017
   Proof eXchange for Theorem Proving, C. Dubois, B. Woltzenlogel Paleo (eds.), pp. 77-93 , volume 262 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association
   BibTex@inproceedings{MRLR:alignments:17, author = "D. M{\"u}ller and C. Rothgang and Y. Liu and F. Rabe", title = "{Alignment-based Translations Across Formal Systems Using Interface Theories}", year = "2017", pages = "77--93", booktitle = "Proof eXchange for Theorem Proving", editor = "C. Dubois and B. {Woltzenlogel Paleo}", publisher = "Open Publishing Association" }
6. TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism, Cezary Kaliszyk, Florian Rabe, Geoff Sutcliffe, 2016
   Workshop on Practical Aspects of Automated Reasoning, P. Fontaine, S. Schulz, J. Urban (eds.), pp. 41-55
   BibTex@inproceedings{KRS:thf1:16, author = "C. Kaliszyk and F. Rabe and G. Sutcliffe", title = "{TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism}", year = "2016", pages = "41--55", booktitle = "Workshop on Practical Aspects of Automated Reasoning", editor = "P. Fontaine and S. Schulz and J. Urban" }
7. A Logic-Independent IDE, Florian Rabe, 2014
   Workshop on User Interfaces for Theorem Provers, C. Benzmüller, B. Woltzenlogel Paleo (eds.), pp. 48-60 , volume 167 of Electronic Notes in Theoretical Computer Science, Elsevier
   BibTex@inproceedings{rabe:ui:14, author = "F. Rabe", title = "{A Logic-Independent IDE}", year = "2014", pages = "48--60", booktitle = "Workshop on User Interfaces for Theorem Provers", editor = "C. Benzm{\"u}ller and B. {Woltzenlogel Paleo}", publisher = "Elsevier" } Slides
8. (Work-in-Progress) An MMT-Based User-Interface, Mihnea Iancu, Florian Rabe, 2012
   Workshop on User Interfaces for Theorem Provers, C. Kaliszyk, C. Lüth (eds.)
   BibTex@inproceedings{IR:ui:12, author = "M. Iancu and F. Rabe", title = "{(Work-in-Progress) An MMT-Based User-Interface}", year = "2012", booktitle = "Workshop on User Interfaces for Theorem Provers", editor = "C. Kaliszyk and C. L{\"u}th" } Slides
9. Representing Isabelle in LF, Florian Rabe, 2010
   Logical Frameworks and Meta-languages: Theory and Practice, K. Crary, M. Miculan (eds.), pp. 85-100 , volume 34 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association
   BibTex@inproceedings{rabe:isalf:10, author = "F. Rabe", title = "{Representing Isabelle in LF}", year = "2010", pages = "85--100", booktitle = "Logical Frameworks and Meta-languages: Theory and Practice", editor = "K. Crary and M. Miculan", publisher = "Open Publishing Association" } Slides
10. A Practical Module System for LF, Florian Rabe, Carsten Schürmann, 2009
    Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), J. Cheney, A. Felty (eds.), pp. 40-48 , volume LFMTP'09 of ACM International Conference Proceeding Series, ACM Press
    BibTex@inproceedings{RS:twelfmod:09, author = "F. Rabe and C. Sch{\"u}rmann", title = "{A Practical Module System for LF}", year = "2009", pages = "40--48", booktitle = "Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP)", editor = "J. Cheney and A. Felty", publisher = "ACM Press" } Slides
11. Representing Model Theory in a Type-Theoretical Logical Framework, Fulya Horozal, Florian Rabe, 2009
    Fourth Workshop on Logical and Semantic Frameworks, with Applications, M. Ayala-Rincón, F. Kamareddine (eds.), pp. 49-65 , volume 256 of Electronic Notes in Theoretical Computer Science, Elsevier
    BibTex@inproceedings{HR:folsound:09, author = "F. Horozal and F. Rabe", title = "{Representing Model Theory in a Type-Theoretical Logical Framework}", year = "2009", pages = "49--65", booktitle = "Fourth Workshop on Logical and Semantic Frameworks, with Applications", editor = "M. Ayala-Rinc{\'o}n and F. Kamareddine", publisher = "Elsevier" }
12. An Exchange Format for Modular Knowledge, Florian Rabe, Michael Kohlhase, 2008
    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, S. Schulz (eds.), pp. 50-68 , volume 418 of CEUR Workshop Proceedings, CEUR-WS.org
    BibTex@inproceedings{RK:keappa:08, author = "F. Rabe and M. Kohlhase", title = "{An Exchange Format for Modular Knowledge}", year = "2008", pages = "50--68", booktitle = "Proceedings of the LPAR Workshops on Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics", editor = "G. Sutcliffe and P. Rudnicki and R. Schmidt and B. Konev and S. Schulz", publisher = "CEUR-WS.org" }
13. Flyspeck in a Semantic Wiki, Christoph Lange, Sean McLaughlin, Florian Rabe, 2008
    Semantic Wiki Workshop, C. Lange, S. Schaffert, H. Skaf-Molli, M. Völkel (eds.), pp. 67-81 , volume 360 of CEUR Workshop Proceedings, CEUR-WS.org
    BibTex@inproceedings{LMR:flyspeck:08, author = "C. Lange and S. McLaughlin and F. Rabe", title = "{Flyspeck in a Semantic Wiki}", year = "2008", pages = "67--81", booktitle = "Semantic Wiki Workshop", editor = "C. Lange and S. Schaffert and H. Skaf-Molli and M. V{\"o}lkel", publisher = "CEUR-WS.org" }
14. Towards Determining the Subset Relation between Propositional Modal Logics, Florian Rabe, 2006
    Proceedings of the FLoC 06 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning, G. Sutcliffe, R. Schmidt, S. Schulz (eds.), pp. 126-140 , volume 192 of CEUR Workshop Proceedings, CEUR-WS.org
    BibTex@inproceedings{rabe:moloss:06, author = "F. Rabe", title = "{Towards Determining the Subset Relation between Propositional Modal Logics}", year = "2006", pages = "126--140", booktitle = "Proceedings of the FLoC 06 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning", editor = "G. Sutcliffe and R. Schmidt and S. Schulz", publisher = "CEUR-WS.org" }
15. A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela$^+$, Florian Rabe, Steffen Schlager, Peter Schmitt, 2005
    Short Paper Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp. 21-27
    BibTex@inproceedings{rabeEA:promela:05, author = "F. Rabe and S. Schlager and P. Schmitt", title = "{A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela$^+$}", year = "2005", pages = "21--27", booktitle = "Short Paper Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning" }

Invited Articles in Collections

1. Representing Logics and Logic Translations, Florian Rabe, 2009
   Ausgezeichnete Informatikdissertationen 2008, D. Wagner et al. (eds.), pp. 201-210 , volume D-9 of Lecture Notes in Informatics, Gesellschaft für Informatik e.V. (GI)
   English title: Outstanding Dissertations in Computer Science 2008
   BibTex@inproceedings{rabe:gi:09, author = "F. Rabe", title = "{Representing Logics and Logic Translations}", year = "2009", note = "English title: Outstanding Dissertations in Computer Science 2008", pages = "201--210", booktitle = "Ausgezeichnete Informatikdissertationen 2008", editor = "D. {Wagner et al.}", publisher = "Gesellschaft f{\"u}r Informatik e.V. (GI)" }

Theses

1. A Scalable Logical Framework, Florian Rabe, 2014
   Dr. habil. thesis, Jacobs University Bremen
   BibTex@phdthesis{rabe:habil:14, type = "Habilitation thesis", author = "F. Rabe", title = "{A Scalable Logical Framework}", year = "2014", note = "see \url{http://kwarc.info/frabe/Research/rabe_habil_14.pdf}", school = "Jacobs University Bremen" }
2. Representing Logics and Logic Translations, Florian Rabe, 2008
   Ph.D. thesis, Jacobs University Bremen
   BibTex@phdthesis{rabe:thesis:08, author = "F. Rabe", title = "{Representing Logics and Logic Translations}", year = "2008", note = "see \url{http://kwarc.info/frabe/Research/phdthesis.pdf}", school = "Jacobs University Bremen" }
3. Representing Logics and Logic Translations (Summary), Florian Rabe, 2008
   Ph.D. thesis, Jacobs University Bremen
   BibTex@phdthesis{rabe:summary:08, author = "F. Rabe", title = "{Representing Logics and Logic Translations (Summary)}", year = "2008", note = "see \url{http://kwarc.info/frabe/Research/phdthesis_summary.pdf}", school = "Jacobs University Bremen" }
4. A Dynamic Logic with Temporal Operators for Promela, Florian Rabe, 2004
   M.Sc. thesis, Universität Karlsruhe, Germany
   BibTex@mastersthesis{rabe:thesis:04, author = "F. Rabe", title = "{A Dynamic Logic with Temporal Operators for Promela}", year = "2004", school = "Universit{\"a}t Karlsruhe, Germany" }

Edited Collections

1. LFMTP 2024: Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice, Florian Rabe, Claudio Sacerdoti Coen, 2024
   volume 404 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association
   BibTex@proceedings{RS:lfmtp:24, title = "{LFMTP 2024: Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice}", year = "2024", note = "see \url{https://cgi.cse.unsw.edu.au/~eptcs/content.cgi?LFMTP2024}", editor = "F. Rabe and C. {Sacerdoti Coen}", publisher = "Open Publishing Association" }
2. Workshop Papers at CICM 2018, O. Hasan, Florian Rabe, 19 others, 2019
   volume 2307 of null, CEUR-WS.org
   BibTex@proceedings{cicm:18:wip, title = "{Workshop Papers at CICM 2018}", year = "2019", note = "see \url{http://ceur-ws.org/Vol-2307/}", editor = "O. Hasan and F. Rabe and 19 others", publisher = "CEUR-WS.org" }
3. Intelligent Computer Mathematics, Florian Rabe, W. Farmer, G. Passmore, A. Youssef, 2018
   volume 11006 of Lecture Notes in Computer Science, Springer
   BibTex@proceedings{RFPY:cicm:18, title = "{Intelligent Computer Mathematics}", year = "2018", note = "see \url{https://www.springer.com/book/9783319968117}", editor = "F. Rabe and W. Farmer and G. Passmore and A. Youssef", publisher = "Springer" }
4. Intelligent Computer Mathematics, H. Geuvers, M. England, O. Hasan, Florian Rabe, O. Teschke, 2017
   volume 10383 of Lecture Notes in Computer Science, Springer
   BibTex@proceedings{GEHRT:cicm:17, title = "{Intelligent Computer Mathematics}", year = "2017", note = "see \url{http://www.springer.com/gp/book/9783319620749}", editor = "H. Geuvers and M. England and O. Hasan and F. Rabe and O. Teschke", publisher = "Springer" }
5. LFMTP: Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice, M. Miculan, Florian Rabe, 2017
   ACM International Conference Proceeding Series, ACM
   BibTex@proceedings{MR:lfmtp:17, title = "{LFMTP: Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice}", year = "2017", note = "see \url{http://dl.acm.org/citation.cfm?id=3130261}", editor = "M. Miculan and F. Rabe", publisher = "ACM" }
6. LFMTP: Work-in-Progress Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice, M. Miculan, Florian Rabe, 2017
   null, University of Udine, Department of Science, Mathematics, Computer Science, and Physics
   BibTex@proceedings{MR:lfmtpwip:17, title = "{LFMTP: Work-in-Progress Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice}", year = "2017", note = "see \url{https://www.dimi.uniud.it/la-ricerca/pubblicazioni/preprints/5.2017/}", editor = "M. Miculan and F. Rabe", publisher = "University of Udine, Department of Science, Mathematics, Computer Science, and Physics" }
7. Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, Florian Rabe, V. Sorge, 2015
   volume 9150 of Lecture Notes in Computer Science, Springer
   BibTex@proceedings{KCKRS:cicm:15, title = "{Intelligent Computer Mathematics}", year = "2015", note = "see \url{http://www.springer.com/gp/book/9783319206141}", editor = "M. Kerber and J. Carette and C. Kaliszyk and F. Rabe and V. Sorge", publisher = "Springer" }
8. Workshops and Work in Progress at CICM 2013, C. Lange, D. Aspinall, J. Carette, J. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, P. Quaresma, Florian Rabe, P. Sojka, I. Whiteside, W. Windsteiger, 2013
   volume 1010 of CEUR Workshop Proceedings, CEUR-WS.org
   BibTex@proceedings{LangeEA:cicmws:13, title = "{Workshops and Work in Progress at CICM 2013}", year = "2013", editor = "C. Lange and D. Aspinall and J. Carette and J. Davenport and A. Kohlhase and M. Kohlhase and P. Libbrecht and P. Quaresma and F. Rabe and P. Sojka and I. Whiteside and W. Windsteiger", publisher = "CEUR-WS.org" }
9. Intelligent Computer Mathematics, J. Davenport, W. Farmer, Florian Rabe, Josef Urban, 2011
   volume 6824 of Lecture Notes in Computer Science, Springer
   BibTex@proceedings{DFRU:cicm:11, title = "{Intelligent Computer Mathematics}", year = "2011", note = "see \url{http://www.springer.com/gp/book/9783319206141}", editor = "J. Davenport and W. Farmer and F. Rabe and J. Urban", publisher = "Springer" }
10. Intelligent Computer Mathematics, Work-in-Progress Proceedings, A. Asperti, J. Davenport, W. Farmer, Florian Rabe, Josef Urban, 2011
    volume UBLCS-2011-04 of Technical Reports of University of Bologna, University of Bologna
    BibTex@proceedings{DFRU:cicmwip:11, title = "{Intelligent Computer Mathematics, Work-in-Progress Proceedings}", year = "2011", editor = "A. Asperti and J. Davenport and W. Farmer and F. Rabe and J. Urban", publisher = "University of Bologna" }
11. LFMTP 2011 - MLPA 2011 Informal Proceedings, H. Geuvers, G. Nadathur, Florian Rabe, Carsten Schürmann, 2011
    BibTex@proceedings{GNRS:lfmtpmlpa:11, title = "{LFMTP 2011 - MLPA 2011 Informal Proceedings}", year = "2011", note = "see \url{http://kwarc.info/frabe/events/mlpa-11/index.html}", editor = "H. Geuvers and G. Nadathur and F. Rabe and C. Sch{\"u}rmann" }
12. MLPA '10: Proceedings of the 2nd Workshop on Modules and Libraries for Proof Assistants, Florian Rabe, Carsten Schürmann, 2010
    BibTex@proceedings{RS:mlpa:10, title = "{MLPA '10: Proceedings of the 2nd Workshop on Modules and Libraries for Proof Assistants}", year = "2010", note = "see \url{http://kwarc.info/frabe/events/mlpa-10.html}", editor = "F. Rabe and C. Sch{\"u}rmann" }
13. MLPA '09: Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants, Florian Rabe, Carsten Schürmann, 2009
    volume 429 of ACM International Conference Proceeding Series, ACM
    BibTex@proceedings{RS:mlpa:09, title = "{MLPA '09: Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants}", year = "2009", editor = "F. Rabe and C. Sch{\"u}rmann", publisher = "ACM" }

Reviews

1. Review of ``Reasoning in Simple Type Theory -- Festschrift in Honor of Peter B. Andrews on His 70th Birthday'', Florian Rabe, 2010
   Bulletin of Symbolic Logic, 16(3):409-411
   BibTex@article{rabe:bslreview:10, author = "F. Rabe", title = "{Review of ``Reasoning in Simple Type Theory -- Festschrift in Honor of Peter B. Andrews on His 70th Birthday''}", year = "2010", pages = "409--411", journal = "Bulletin of Symbolic Logic", volume = "16", number = "3" }

Other Research Publications (most of them lightly refereed)

1. Aligning Mathematical Concepts Across Libraries, Florian Rabe, 2024
   Dagstuhl Seminar on Automated mathematics, A. Bauer, Katja Berčič, N. Thiéry, Florian Rabe, J. Taslak (eds.), pp. 18-20 , volume 23401 of Dagstuhl Reports, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
   BibTex@inproceedings{rabe:dagstuhl:alignments:24, author = "F. Rabe", title = "{Aligning Mathematical Concepts Across Libraries}", year = "2024", pages = "18--20", booktitle = "Dagstuhl Seminar on Automated mathematics", editor = "A. Bauer and K. Ber{\v{c}}i{\v{c}} and N. Thi{\'e}ry and F. Rabe and J. Taslak", publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik" }
2. Aspects of Knowledge for Next Generation Systems, Florian Rabe, 2024
   The Next Generation of Deduction Systems: From Composition to Compositionality, M. Bonacina, P. Fontaine, C. Nalon, C. Schon, M. Desharnais (eds.), pp. 144-145 , volume 23471 of Dagstuhl Reports, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
   BibTex@inproceedings{rabe:dagstuhl:nextgen:24, author = "F. Rabe", title = "{Aspects of Knowledge for Next Generation Systems}", year = "2024", pages = "144--145", booktitle = "The Next Generation of Deduction Systems: From Composition to Compositionality", editor = "M. Bonacina and P. Fontaine and C. Nalon and C. Schon and M. Desharnais", publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik" }
3. Three Case Studies on Realms, Florian Rabe, Franzika Weber, 2022
   Intelligent Computer Mathematics, Informal Proceedings, K. Buzzard, T. Kutsia (eds.), pp. 46-51 , volume 6584 of RISC Technical Report, Research Institute for Symbolic Computation
   BibTex@inproceedings{RW:realms:22, author = "F. Rabe and F. Weber", title = "{Three Case Studies on Realms}", year = "2022", pages = "46--51", booktitle = "Intelligent Computer Mathematics, Informal Proceedings", editor = "K. Buzzard and T. Kutsia", publisher = "Research Institute for Symbolic Computation" }
4. The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems, Katja Berčič, J. Carette, W. Farmer, Dennis Müller, Michael Kohlhase, Florian Rabe, Y. Sharoda, 2020
   BibTex@unpublished{tetrapod:survey:20, author = "K. Ber{\v{c}}i{\v{c}} and J. Carette and W. Farmer and D. M{\"u}ller and M. Kohlhase and F. Rabe and Y. Sharoda", title = "{The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems}", year = "2020", note = "see \url{https://arxiv.org/abs/2002.04955}" }
5. How to Leverage a Large Dataset of Formalized Mathematics with Machine Learning?, Dennis Müller, Michael Kohlhase, Florian Rabe, 2019
   Conference on Artificial Intelligence and Theorem Proving, T. Hales, C. Kaliszyk, R. Kumar, S. Schulz, J. Urban (eds.)
   BibTex@inproceedings{MKR:aimathhub:19, author = "D. M{\"u}ller and M. Kohlhase and F. Rabe", title = "{How to Leverage a Large Dataset of Formalized Mathematics with Machine Learning?}", year = "2019", booktitle = "Conference on Artificial Intelligence and Theorem Proving", editor = "T. Hales and C. Kaliszyk and R. Kumar and S. Schulz and J. Urban" }
6. Structuring Theories with Implicit Morphisms, Dennis Müller, Florian Rabe, 2018
   Workshop on Algebraic Development Techniques, J. Fiadeiro, I. Tutu (eds.)
   BibTex@inproceedings{MR:implicit:18, author = "D. M{\"u}ller and F. Rabe", title = "{Structuring Theories with Implicit Morphisms}", year = "2018", booktitle = "Workshop on Algebraic Development Techniques", editor = "J. Fiadeiro and I. Tutu" }
7. The MMT Perspective on Conservativity, Florian Rabe, 2017
   Logical and Semantic Frameworks, with Applications, S. Alves, R. Wassermann (eds.), pp. 17-33
   BibTex@inproceedings{rabe:cons:16, author = "F. Rabe", title = "{The MMT Perspective on Conservativity}", year = "2017", pages = "17--33", booktitle = " Logical and Semantic Frameworks, with Applications", editor = "S. Alves and R. Wassermann" } Slides
8. A Standard for Aligning Mathematical Concepts, Cezary Kaliszyk, Michael Kohlhase, Dennis Müller, Florian Rabe, 2016
   Work in Progress at CICM 2016, A. Kohlhase, M. Kohlhase, P. Libbrecht, B. Miller, F. Tompa, A. Naummowicz, W. Neuper, P. Quaresma, M. Suda (eds.), pp. 229-244 , volume 1785 of CEUR Workshop Proceedings, CEUR-WS.org
   BibTex@inproceedings{KKMR:alignments:16, author = "C. Kaliszyk and M. Kohlhase and D. M{\"u}ller and F. Rabe", title = "{A Standard for Aligning Mathematical Concepts}", year = "2016", pages = "229--244", booktitle = "Work in Progress at CICM 2016", editor = "A. Kohlhase and M. Kohlhase and P. Libbrecht and B. Miller and F. Tompa and A. Naummowicz and W. Neuper and P. Quaresma and M. Suda", publisher = "CEUR-WS.org" }
9. Breakout session on A standard for system integration and proof interchange, R. Kumar, Florian Rabe, 2016
   Dagstuhl Seminar on Universality of Proofs, G. Dowek, C. Dubois, B. Pientka, Florian Rabe (eds.), pp. 94-94 , volume 16421 of Dagstuhl Reports, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
   BibTex@inproceedings{rabe:mmt:standard:16, author = "R. Kumar and F. Rabe", title = "{Breakout session on A standard for system integration and proof interchange}", year = "2016", pages = "94--94", booktitle = "Dagstuhl Seminar on Universality of Proofs", editor = "G. Dowek and C. Dubois and B. Pientka and F. Rabe", publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik" }
10. MMT: A UniFormal Approach to Knowledge Representation, Florian Rabe, 2016
    Dagstuhl Seminar on Universality of Proofs, G. Dowek, C. Dubois, B. Pientka, Florian Rabe (eds.), pp. 88-88 , volume 16421 of Dagstuhl Reports, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
    BibTex@inproceedings{rabe:mmt:universality:16, author = "F. Rabe", title = "{MMT: A UniFormal Approach to Knowledge Representation}", year = "2016", pages = "88--88", booktitle = "Dagstuhl Seminar on Universality of Proofs", editor = "G. Dowek and C. Dubois and B. Pientka and F. Rabe", publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik" }
11. Selecting Colimits for Parameterisation and Networks of Specifications, Mihai Codescu, Till Mossakowski, Florian Rabe, 2016
    Workshop on Algebraic Development Techniques, M. Roggenbach, P. James (eds.)
    BibTex@inproceedings{CMR:selecting:16, author = "M. Codescu and T. Mossakowski and F. Rabe", title = "{Selecting Colimits for Parameterisation and Networks of Specifications}", year = "2016", booktitle = "Workshop on Algebraic Development Techniques", editor = "M. Roggenbach and P. James" } Slides
12. MMT Objects, Florian Rabe, 2014
    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, S. Watt (eds.) , volume 1186 of CEUR Workshop Proceedings, CEUR-WS.org
    BibTex@inproceedings{rabe:mmtobjects:14, author = "F. Rabe", title = "{MMT Objects}", year = "2014", booktitle = "Workshops and Work in Progress at CICM 2014: OpenMath Workshop", editor = "M. England and J. Davenport and A. Kohlhase and M. Kohlhase and P. Libbrecht and W. Neuper and P. Quaresma and A. Sexton and P. Sojka and J. Urban and S. Watt", publisher = "CEUR-WS.org" } Slides
13. The Scala-REPL + MMT as a lightweight mathematical user interface, Mihnea Iancu, Felix Mance, Florian Rabe, 2013
    Workshops and Work in Progress at CICM 2013: Mathematical User Interfaces (MathUI), C. Lange, D. Aspinall, J. Carette, J. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, P. Quaresma, Florian Rabe, P. Sojka, I. Whiteside, W. Windsteiger (eds.) , volume 1010 of CEUR Workshop Proceedings, CEUR-WS.org
    BibTex@inproceedings{IMR:mmtrepl:13, author = "M. Iancu and F. Mance and F. Rabe", title = "{The Scala-REPL + MMT as a lightweight mathematical user interface}", year = "2013", booktitle = "Workshops and Work in Progress at CICM 2013: Mathematical User Interfaces (MathUI)", editor = "C. Lange and D. Aspinall and J. Carette and J. Davenport and A. Kohlhase and M. Kohlhase and P. Libbrecht and P. Quaresma and F. Rabe and P. Sojka and I. Whiteside and W. Windsteiger", publisher = "CEUR-WS.org" }
14. Compiling Logics, Mihai Codescu, Fulya Horozal, Till Mossakowski, Florian Rabe, 2012
    Workshop on Algebraic Development Techniques
    BibTex@inproceedings{CHMR:compiling:12, author = "M. Codescu and F. Horozal and T. Mossakowski and F. Rabe", title = "{Compiling Logics}", year = "2012", booktitle = "Workshop on Algebraic Development Techniques" }
15. Mechanically Verifying Logic Translations, Florian Rabe, Kristina Sojakova, 2012
    Workshop on Algebraic Development Techniques
    BibTex@inproceedings{RS:vertrans:12, author = "F. Rabe and K. Sojakova", title = "{Mechanically Verifying Logic Translations}", year = "2012", booktitle = "Workshop on Algebraic Development Techniques" }
16. Representing CASL in a Proof-Theoretical Logical Framework, Mihai Codescu, Fulya Horozal, Iulia Ignatov, Florian Rabe, 2012
    Workshop on Algebraic Development Techniques
    BibTex@inproceedings{CHIR:casl:12, author = "M. Codescu and F. Horozal and I. Ignatov and F. Rabe", title = "{Representing CASL in a Proof-Theoretical Logical Framework}", year = "2012", booktitle = "Workshop on Algebraic Development Techniques" }
17. Representing Categories of Theories in a Proof-Theoretical Logical Framework, Fulya Horozal, Florian Rabe, 2012
    Workshop on Algebraic Development Techniques
    BibTex@inproceedings{HR:patterns:12, author = "F. Horozal and F. Rabe", title = "{Representing Categories of Theories in a Proof-Theoretical Logical Framework}", year = "2012", booktitle = "Workshop on Algebraic Development Techniques" }
18. Extending OpenMath with Sequences, Fulya Horozal, Michael Kohlhase, Florian Rabe, 2011
    Intelligent Computer Mathematics, Work-in-Progress Proceedings, A. Asperti, J. Davenport, W. Farmer, F. Rabe, J. Urban (eds.), pp. 58-72 , volume UBLCS-2011-04 of Technical Report, University of Bologna, University of Bologna
    BibTex@inproceedings{HKR:sequences:11, author = "F. Horozal and M. Kohlhase and F. Rabe", title = "{Extending OpenMath with Sequences}", year = "2011", pages = "58--72", booktitle = "Intelligent Computer Mathematics, Work-in-Progress Proceedings", editor = "A. Asperti and J. Davenport and W. Farmer and F. Rabe and J. Urban", publisher = "University of Bologna" }
19. Translating the Mizar Mathematical Library into OMDoc format, Mihnea Iancu, Michael Kohlhase, Florian Rabe, 2011
    TechReport KWARC Report-01/11, Jacobs University Bremen
    BibTex@techreport{IKR:mizar:11, author = "M. Iancu and M. Kohlhase and F. Rabe", title = "{Translating the Mizar Mathematical Library into OMDoc format}", year = "2011", institution = "Jacobs University Bremen", number = "KWARC Report-01/11" }
20. A Proof Theoretic Interpretation of Model Theoretic Hiding, Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe, 2010
    Workshop on Algebraic Development Techniques
    BibTex@inproceedings{CHKMR:hiding:10, author = "M. Codescu and F. Horozal and M. Kohlhase and T. Mossakowski and F. Rabe", title = "{A Proof Theoretic Interpretation of Model Theoretic Hiding}", year = "2010", booktitle = "Workshop on Algebraic Development Techniques" }
21. Interactive Documents as Interfaces to Computer Algebra Systems: JOBAD and Wolfram|Alpha, Catalin David, Christoph Lange, Florian Rabe, 2010
    CALCULEMUS (Emerging Trends), D. Delahaye, R. Rioboo (eds.), pp. 13-30 , Technical Reports of CEDRIC (CNAM/ENSIIE), Centre d'Étude et de Recherche en Informatique du CNAM (Cédric)
    BibTex@inproceedings{DLR:jobad:10, author = "C. David and C. Lange and F. Rabe", title = "{Interactive Documents as Interfaces to Computer Algebra Systems: JOBAD and Wolfram|Alpha}", year = "2010", pages = "13--30", booktitle = "CALCULEMUS (Emerging Trends)", editor = "D. Delahaye and R. Rioboo", publisher = "Centre d'{\'E}tude et de Recherche en Informatique du CNAM (C{\'e}dric)" }
22. JOBAD/MMT -- Interactive Mathematics, Catalin David, Michael Kohlhase, Christoph Lange, Florian Rabe, Vyacheslav Zholudev, 2010
    AI Mashup Challenge at ESWC, A. Giurca, B. Endres-Niggemeyer, Christoph Lange, L. Maicher, P. Hitzler (eds.)
    BibTex@inproceedings{DKLRZ:jobadmmt:10, author = "C. David and M. Kohlhase and C. Lange and F. Rabe and V. Zholudev", title = "{JOBAD/MMT -- Interactive Mathematics}", year = "2010", note = "see \url{http://sites.google.com/a/fh-hannover.de/aimashup/home/jobad}", booktitle = "AI Mashup Challenge at ESWC", editor = "A. Giurca and B. Endres-Niggemeyer and C. Lange and L. Maicher and P. Hitzler" }
23. Structuring Theories with Partial Morphisms, Stefania Dumbrava, Florian Rabe, 2010
    Workshop on Algebraic Development Techniques
    BibTex@inproceedings{DR:filtering:10, author = "S. Dumbrava and F. Rabe", title = "{Structuring Theories with Partial Morphisms}", year = "2010", booktitle = "Workshop on Algebraic Development Techniques" }
24. Towards Logical Frameworks in the Heterogeneous Tool Set Hets, Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe, Kristina Sojakova, 2010
    Workshop on Algebraic Development Techniques
    BibTex@inproceedings{CHKMRS:lfhets:10, author = "M. Codescu and F. Horozal and M. Kohlhase and T. Mossakowski and F. Rabe and K. Sojakova", title = "{Towards Logical Frameworks in the Heterogeneous Tool Set Hets}", year = "2010", booktitle = "Workshop on Algebraic Development Techniques" }
25. A Better Role System for OpenMath, Florian Rabe, Michael Kohlhase, 2009
    Proceedings of the OpenMath workshop
    BibTex@inproceedings{RK:roles:09, author = "F. Rabe and M. Kohlhase", title = "{A Better Role System for OpenMath}", year = "2009", booktitle = "Proceedings of the OpenMath workshop" }
26. Notations for Active Mathematical Documents, Michael Kohlhase, Christoph Lange, Christine Müller, Normen Müller, Florian Rabe, 2009
    TechReport 2009-1, Jacobs University Bremen
    BibTex@techreport{KLMMR:notations-tr:2009, author = "M. Kohlhase and C. Lange and C. M{\"u}ller and N. M{\"u}ller and F. Rabe", title = "{Notations for Active Mathematical Documents}", year = "2009", institution = "Jacobs University Bremen", number = "2009-1" }
27. Semantics of OpenMath and MathML 3, Michael Kohlhase, Florian Rabe, 2009
    Proceedings of the OpenMath workshop
    BibTex@inproceedings{KR:omsemantics:09, author = "M. Kohlhase and F. Rabe", title = "{Semantics of OpenMath and MathML 3}", year = "2009", booktitle = "Proceedings of the OpenMath workshop" }
28. Evaluation of Systems for Higher-order Logic (ESHOL), Christoph Benzmüller, Florian Rabe, Carsten Schürmann, Geoff Sutcliffe, 2008
    Workshop on Practical Aspects of Automated Reasoning at IJCAR 2008, B. Konev, R. Schmidt, S. Schulz (eds.), pp. 22-23 , volume 373 of CEUR Workshop Proceedings, CEUR-WS.org
    BibTex@inproceedings{BRSS:eshol:08, author = "C. Benzm{\"u}ller and F. Rabe and C. Sch{\"u}rmann and G. Sutcliffe", title = "{Evaluation of Systems for Higher-order Logic (ESHOL)}", year = "2008", pages = "22--23", booktitle = "Workshop on Practical Aspects of Automated Reasoning at IJCAR 2008", editor = "B. Konev and R. Schmidt and S. Schulz", publisher = "CEUR-WS.org" }
29. Translating Dependently-Typed Logic to First-Order Logic, Kristina Sojakova, Florian Rabe, 2008
    Workshop on Algebraic Development Techniques, A. Corradini, U. Montanari (eds.)
    BibTex@inproceedings{SR:dfol_fol_abs:08, author = "K. Sojakova and F. Rabe", title = "{Translating Dependently-Typed Logic to First-Order Logic}", year = "2008", booktitle = "Workshop on Algebraic Development Techniques", editor = "A. Corradini and U. Montanari" }
30. OMDoc Theory Graphs Revisited, Florian Rabe, 2007
    Proceedings of the OpenMath/JEM workshop
    BibTex@inproceedings{rabe:graphs:07, author = "F. Rabe", title = "{OMDoc Theory Graphs Revisited}", year = "2007", booktitle = "Proceedings of the OpenMath/JEM workshop" }
31. Presenting Mathematical Content with Flexible Elisions, Michael Kohlhase, Christoph Lange, Florian Rabe, 2007
    Proceedings of the OpenMath/JEM workshop
    BibTex@inproceedings{rabeEA:elisions:07, author = "M. Kohlhase and C. Lange and F. Rabe", title = "{Presenting Mathematical Content with Flexible Elisions}", year = "2007", booktitle = "Proceedings of the OpenMath/JEM workshop" }
32. A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela$^+$, Florian Rabe, Steffen Schlager, Peter Schmitt, 2005
    Proceedings of the 17th Nordic Workshop on Programming Theory
    BibTex@inproceedings{rabeEA:promela1:05, author = "F. Rabe and S. Schlager and P. Schmitt", title = "{A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela$^+$}", year = "2005", booktitle = "Proceedings of the 17th Nordic Workshop on Programming Theory" }

Textbook-Style Lecture Notes

1. Lecture Notes on Algorithms and Data Structures, Florian Rabe, 2017
   BibTex@book{rabe:notes:ad, author = "F. Rabe", title = "{Lecture Notes on Algorithms and Data Structures}", year = "2017", note = "see \url{https://github.com/florian-rabe/Teaching/tree/master/AaDS_17}" }
2. Lecture Notes on Secure and Dependable Systems, Florian Rabe, 2017
   BibTex@book{rabe:notes:sd, author = "F. Rabe", title = "{Lecture Notes on Secure and Dependable Systems}", year = "2017", note = "see \url{https://github.com/florian-rabe/Teaching/tree/master/SaDS_17}" }
3. Integrated Lecture Notes on Logic (2008--2016), Florian Rabe, 2016
   BibTex@book{rabe:notes:logic, author = "F. Rabe", title = "{Integrated Lecture Notes on Logic (2008--2016)}", year = "2016", note = "see \url{https://github.com/florian-rabe/Teaching/blob/master/logic/notes_logic.pdf}" }

Selected Service Documents

1. Advice for Students, Florian Rabe, 2018
   BibTex@misc{rabe:service:students, author = "F. Rabe", title = "{Advice for Students}", year = "2018", note = "see \url{https://github.com/florian-rabe/Teaching/blob/master/general/advice_for_students.pdf}" }
2. Advice for PC Chairs, Florian Rabe, 2011
   BibTex@misc{rabe:service:pc, author = "F. Rabe", title = "{Advice for PC Chairs}", year = "2011" }