Edit Profile (opens in new tab) Rabe, Florian Compute Distance To: Compute Author ID: rabe.florian Published as: Rabe, Florian Homepage: https://kwarc.info/people/frabe/ External Links: MGP · ORCID · dblp Documents Indexed: 64 Publications since 2006 4 Contributions as Editor Co-Authors: 54 Co-Authors with 55 Joint Publications 907 Co-Co-Authors all top 5 Co-Authors 12 single-authored 30 Kohlhase, Michael 10 Horozal, Fulya 10 Müller, Dennis 5 Codescu, Mihai 5 Mossakowski, Till 4 Iancu, Mihnea 4 Kaliszyk, Cezary 4 Sacerdoti Coen, Claudio 4 Wiesing, Tom 3 Farmer, William M. 3 Sojakova, Kristina 2 Awodey, Steve 2 Berčič, Katja 2 Carette, Jacques 2 Pfeiffer, Markus 2 Rothgang, Colin 2 Sutcliffe, Geoff 2 Thiéry, Nicolas Marc 2 Urban, Josef 1 Amann, Kai 1 Benzmüller, Christoph Ewald 1 Condoluci, Andrea 1 Davenport, James Harold 1 De Feo, Luca 1 Dehaye, Paul-Olivier 1 England, Matthew 1 Gauthier, Thibault 1 Geuvers, Jan Herman 1 Giceva, Jana 1 Hasan, Osman 1 Iacob, Alin 1 Jakubauskas, Aivaras 1 Jucovschi, Constantin 1 Kerber, Manfred 1 Konovalov, Olexandr 1 Korniłowicz, Artur 1 Lange, Christoph 1 Lelièvre, Samuel 1 Mance, Felix 1 Marcus, Richard 1 Müller, Christine 1 Owre, Sam 1 Passmore, Grant Olney 1 Pudlák, Pavel 1 Roux, Navid 1 Schaefer, Jan Frederik 1 Sharoda, Yasmine 1 Shen, Weina 1 Sorge, Volker 1 Teschke, Olaf 1 Vasil’ev, Victor V. 1 Wenzel, Makarius 1 Youssef, Abdou S. 1 Zholudev, Vyacheslav all top 5 Serials 4 Lecture Notes in Computer Science 3 ACM Transactions on Computational Logic 2 Theoretical Computer Science 2 Journal of Automated Reasoning 2 MSCS. Mathematical Structures in Computer Science 1 The Mathematical Intelligencer 1 Information and Computation 1 Journal of Logic and Computation 1 Journal of Applied Logic 1 Mathematics in Computer Science 1 Logica Universalis 1 Logical Methods in Computer Science 1 Journal of Formalized Reasoning Fields 62 Computer science (68-XX) 18 Mathematical logic and foundations (03-XX) 6 General and overarching topics; collections (00-XX) 2 Category theory; homological algebra (18-XX) 1 History and biography (01-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 52 Publications have been cited 227 times in 95 Documents Cited by ▼ Year ▼ A scalable module system. Zbl 1358.68283Rabe, Florian; Kohlhase, Michael 30 2013 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 17 2013 The MMT API: a generic MKM system. Zbl 1390.68626Rabe, Florian 17 2013 Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian 16 2011 Formalising foundations of mathematics. Zbl 1242.03031Iancu, Mihnea; Rabe, Florian 11 2011 A logical framework combining model and proof theory. Zbl 1326.03082Rabe, Florian 8 2013 Representing model theory in a type-theoretical logical framework. Zbl 1236.03027Horozal, Fulya; Rabe, Florian 8 2011 Notations for living mathematical documents. Zbl 1166.00304Kohlhase, Michael; Müller, Christine; Rabe, Florian 7 2008 How to identify, translate and combine logics? Zbl 1444.03121Rabe, Florian 7 2017 Towards logical frameworks in the heterogeneous tool set Hets. Zbl 1278.68286Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina 7 2012 THF0 – the core of the TPTP language for higher-order logic. Zbl 1165.68447Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff 7 2008 Towards MKM in the large: modular representation and scalable software architecture. Zbl 1278.68297Kohlhase, Michael; Rabe, Florian; Zholudev, Vyacheslav 6 2010 Extending MKM formats at the statement level. Zbl 1278.68293Horozal, Fulya; Kohlhase, Michael; Rabe, Florian 6 2012 A foundational view on integration problems. Zbl 1278.68289Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio 6 2011 Flexary operators for formalized mathematics. Zbl 1304.68171Horozal, Fulya; Rabe, Florian; Kohlhase, Michael 5 2014 Integrating web services into active mathematical documents. Zbl 1247.68314Giceva, Jana; Lange, Christoph; Rabe, Florian 5 2009 Towards knowledge management for HOL Light. Zbl 1304.68158Kaliszyk, Cezary; Rabe, Florian 4 2014 A survey of languages for formalizing mathematics. Zbl 1455.68257Kaliszyk, Cezary; Rabe, Florian 4 2020 Logical relations for a logical framework. Zbl 1353.68252Rabe, Florian; Sojakova, Kristina 3 2013 Generic literals. Zbl 1417.68216Rabe, Florian 3 2015 A query language for formal mathematical libraries. Zbl 1359.68272Rabe, Florian 3 2012 A modular type reconstruction algorithm. Zbl 1407.68440Rabe, Florian 3 2018 Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian 3 2017 Kripke semantics for Martin-Löf’s extensional type theory. Zbl 1237.03007Awodey, Steve; Rabe, Florian 2 2011 A universal machine for biform theory graphs. Zbl 1278.68267Kohlhase, Michael; Mance, Felix; Rabe, Florian 2 2013 Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Zbl 1316.68015 2 2015 Interoperability in the OpenDreamKit project: the math-in-the-middle approach. Zbl 1344.68268Dehaye, Paul-Olivier; Iancu, Mihnea; Kohlhase, Michael; Konovalov, Alexander; Lelièvre, Samuel; Müller, Dennis; Pfeiffer, Markus; Rabe, Florian; Thiéry, Nicolas M.; Wiesing, Tom 2 2016 Kripke semantics for Martin-Löf’s extensional type theory. Zbl 1246.03022Awodey, Steve; Rabe, Florian 2 2009 Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Zbl 1218.68014 2 2011 The Coq library as a theory graph. Zbl 1428.68344Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio 2 2019 Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 1497.68550Wiesing, Tom; Kohlhase, Michael; Rabe, Florian 2 2017 QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343Kohlhase, Michael; Rabe, Florian 2 2016 First-order logic with dependent types. Zbl 1222.03016Rabe, Florian 2 2006 How to calculate with nondeterministic functions. Zbl 1434.68078Bird, Richard; Rabe, Florian 2 2019 Representing structural language features in formal meta-languages. Zbl 1455.68268Müller, Dennis; Rabe, Florian; Rothgang, Colin; Kohlhase, Michael 2 2020 Representing model theory in a type-theoretical logical framework. Zbl 1291.03068Horozal, Fulya; Rabe, Florian 1 2009 Making PVS accessible to generic services by interpretation in a universal format. Zbl 1484.68311Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian 1 2017 The future of logic: foundation-independence. Zbl 1436.03179Rabe, Florian 1 2016 Formal logic definitions for interchange languages. Zbl 1417.68206Horozal, Fulya; Rabe, Florian 1 2015 Compiling logics. Zbl 1394.68071Codescu, Mihai; Horozal, Fulya; Jakubauskas, Aivaras; Mossakowski, Till; Rabe, Florian 1 2013 Morphism axioms. Zbl 1373.03132Rabe, Florian 1 2017 A proof theoretic interpretation of model theoretic hiding. Zbl 1278.68202Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian 1 2012 Solving the $100 modal logic challenge. Zbl 1161.03302Rabe, Florian; Pudlák, Petr; Sutcliffe, Geoff; Shen, Weina 1 2009 Canonical selection of colimits. Zbl 1496.68203Mossakowski, Till; Rabe, Florian; Codescu, Mihai 1 2017 Towards a unified mathematical data infrastructure: database and interface generation. Zbl 1428.68356Berčič, Katja; Kohlhase, Michael; Rabe, Florian 1 2019 Relational data across mathematical libraries. Zbl 1428.68352Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius 1 2019 Diagram combinators in MMT. Zbl 1428.68353Rabe, Florian; Sharoda, Yasmine 1 2019 Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13–17, 2018. Proceedings. Zbl 1392.68030 1 2018 Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Zbl 1364.68010 1 2017 Lax theory morphisms. Zbl 1367.03061Rabe, Florian 1 2015 Experiences from exporting major proof assistant libraries. Zbl 07461271Kohlhase, Michael; Rabe, Florian 1 2021 Theories as types. Zbl 06958124Müller, Dennis; Rabe, Florian; Kohlhase, Michael 1 2018 Experiences from exporting major proof assistant libraries. Zbl 07461271Kohlhase, Michael; Rabe, Florian 1 2021 A survey of languages for formalizing mathematics. Zbl 1455.68257Kaliszyk, Cezary; Rabe, Florian 4 2020 Representing structural language features in formal meta-languages. Zbl 1455.68268Müller, Dennis; Rabe, Florian; Rothgang, Colin; Kohlhase, Michael 2 2020 The Coq library as a theory graph. Zbl 1428.68344Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio 2 2019 How to calculate with nondeterministic functions. Zbl 1434.68078Bird, Richard; Rabe, Florian 2 2019 Towards a unified mathematical data infrastructure: database and interface generation. Zbl 1428.68356Berčič, Katja; Kohlhase, Michael; Rabe, Florian 1 2019 Relational data across mathematical libraries. Zbl 1428.68352Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius 1 2019 Diagram combinators in MMT. Zbl 1428.68353Rabe, Florian; Sharoda, Yasmine 1 2019 A modular type reconstruction algorithm. Zbl 1407.68440Rabe, Florian 3 2018 Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13–17, 2018. Proceedings. Zbl 1392.68030 1 2018 Theories as types. Zbl 06958124Müller, Dennis; Rabe, Florian; Kohlhase, Michael 1 2018 How to identify, translate and combine logics? Zbl 1444.03121Rabe, Florian 7 2017 Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian 3 2017 Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 1497.68550Wiesing, Tom; Kohlhase, Michael; Rabe, Florian 2 2017 Making PVS accessible to generic services by interpretation in a universal format. Zbl 1484.68311Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian 1 2017 Morphism axioms. Zbl 1373.03132Rabe, Florian 1 2017 Canonical selection of colimits. Zbl 1496.68203Mossakowski, Till; Rabe, Florian; Codescu, Mihai 1 2017 Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Zbl 1364.68010 1 2017 Interoperability in the OpenDreamKit project: the math-in-the-middle approach. Zbl 1344.68268Dehaye, Paul-Olivier; Iancu, Mihnea; Kohlhase, Michael; Konovalov, Alexander; Lelièvre, Samuel; Müller, Dennis; Pfeiffer, Markus; Rabe, Florian; Thiéry, Nicolas M.; Wiesing, Tom 2 2016 QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343Kohlhase, Michael; Rabe, Florian 2 2016 The future of logic: foundation-independence. Zbl 1436.03179Rabe, Florian 1 2016 Generic literals. Zbl 1417.68216Rabe, Florian 3 2015 Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Zbl 1316.68015 2 2015 Formal logic definitions for interchange languages. Zbl 1417.68206Horozal, Fulya; Rabe, Florian 1 2015 Lax theory morphisms. Zbl 1367.03061Rabe, Florian 1 2015 Flexary operators for formalized mathematics. Zbl 1304.68171Horozal, Fulya; Rabe, Florian; Kohlhase, Michael 5 2014 Towards knowledge management for HOL Light. Zbl 1304.68158Kaliszyk, Cezary; Rabe, Florian 4 2014 A scalable module system. Zbl 1358.68283Rabe, Florian; Kohlhase, Michael 30 2013 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 17 2013 The MMT API: a generic MKM system. Zbl 1390.68626Rabe, Florian 17 2013 A logical framework combining model and proof theory. Zbl 1326.03082Rabe, Florian 8 2013 Logical relations for a logical framework. Zbl 1353.68252Rabe, Florian; Sojakova, Kristina 3 2013 A universal machine for biform theory graphs. Zbl 1278.68267Kohlhase, Michael; Mance, Felix; Rabe, Florian 2 2013 Compiling logics. Zbl 1394.68071Codescu, Mihai; Horozal, Fulya; Jakubauskas, Aivaras; Mossakowski, Till; Rabe, Florian 1 2013 Towards logical frameworks in the heterogeneous tool set Hets. Zbl 1278.68286Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina 7 2012 Extending MKM formats at the statement level. Zbl 1278.68293Horozal, Fulya; Kohlhase, Michael; Rabe, Florian 6 2012 A query language for formal mathematical libraries. Zbl 1359.68272Rabe, Florian 3 2012 A proof theoretic interpretation of model theoretic hiding. Zbl 1278.68202Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian 1 2012 Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian 16 2011 Formalising foundations of mathematics. Zbl 1242.03031Iancu, Mihnea; Rabe, Florian 11 2011 Representing model theory in a type-theoretical logical framework. Zbl 1236.03027Horozal, Fulya; Rabe, Florian 8 2011 A foundational view on integration problems. Zbl 1278.68289Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio 6 2011 Kripke semantics for Martin-Löf’s extensional type theory. Zbl 1237.03007Awodey, Steve; Rabe, Florian 2 2011 Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Zbl 1218.68014 2 2011 Towards MKM in the large: modular representation and scalable software architecture. Zbl 1278.68297Kohlhase, Michael; Rabe, Florian; Zholudev, Vyacheslav 6 2010 Integrating web services into active mathematical documents. Zbl 1247.68314Giceva, Jana; Lange, Christoph; Rabe, Florian 5 2009 Kripke semantics for Martin-Löf’s extensional type theory. Zbl 1246.03022Awodey, Steve; Rabe, Florian 2 2009 Representing model theory in a type-theoretical logical framework. Zbl 1291.03068Horozal, Fulya; Rabe, Florian 1 2009 Solving the $100 modal logic challenge. Zbl 1161.03302Rabe, Florian; Pudlák, Petr; Sutcliffe, Geoff; Shen, Weina 1 2009 Notations for living mathematical documents. Zbl 1166.00304Kohlhase, Michael; Müller, Christine; Rabe, Florian 7 2008 THF0 – the core of the TPTP language for higher-order logic. Zbl 1165.68447Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff 7 2008 First-order logic with dependent types. Zbl 1222.03016Rabe, Florian 2 2006 all cited Publications top 5 cited Publications all top 5 Cited by 143 Authors 29 Rabe, Florian 26 Kohlhase, Michael 8 Horozal, Fulya 8 Kaliszyk, Cezary 6 Iancu, Mihnea 6 Korniłowicz, Artur 5 Pąk, Karol 4 Benzmüller, Christoph Ewald 4 Farmer, William M. 4 Gauthier, Thibault 4 Kohlhase, Andrea 4 Mossakowski, Till 4 Naumowicz, Adam 4 Sacerdoti Coen, Claudio 4 Sutcliffe, Geoff 3 Carette, Jacques 3 Codescu, Mihai 3 Grabowski, Adam 3 Müller, Dennis 3 Urban, Josef 3 Wiesing, Tom 2 Bancerek, Grzegorz 2 Bauer, Andrej 2 Berčič, Katja 2 Brown, Chad Edward 2 Byliński, Czesław 2 Foster, Simon 2 Guidi, Ferruccio 2 Jucovschi, Constantin 2 Lange, Christoph 2 Matuszewski, Roman 2 Sojakova, Kristina 2 Sperber, Wolfram 1 Adams, Robin 1 Alessi, Fabio 1 Auer, Sören 1 Awodey, Steve 1 Barbosa, Luís Soares 1 Baumeister, Hubert 1 Bettaz, Mohamed 1 Burel, Guillaume 1 Bury, Guillaume 1 Carter, Nathan C. 1 Cauderlier, Raphaël 1 Cave, Andrew 1 Chiang, Tsung-Ju 1 Chihani, Zakaria 1 Ciaffaglione, Alberto 1 De Lon, Adrian 1 Dehaye, Paul-Olivier 1 Delahaye, David 1 Di Gianantonio, Pietro 1 Diaconescu, Răzvan 1 Dundua, Besik 1 Elizarov, A. M. 1 Freitas, Leo 1 Fürsich, Michael 1 Futatsugi, Kokichi 1 Giceva, Jana 1 Ginev, Deyan 1 Gligorić, Miloš V. 1 Halmagrand, Pierre 1 Haselwarter, Philipp G. 1 Hellström, Lars 1 Henriques, Pedro Rangel 1 Hermant, Olivier 1 Holub, Štěpán 1 Honsell, Furio 1 Huber, Simon 1 Iacob, Alin 1 Jucovshi, Constantin 1 Kaposi, Ambrus 1 Kirillovich, Aleksandr Vital’evich 1 Koepke, Peter 1 Konovalov, Olexandr 1 Koprucki, Thomas 1 Kutsia, Temur 1 Lelièvre, Samuel 1 Lenisa, Marina 1 Lewis, Robert Y. 1 Li, Junyi Jessy 1 Lipachëv, E. K. 1 Lipton, James B. 1 Lorenzen, Anton 1 Luo, Zhaohui 1 Maouche, Mourad 1 Marin, Mircea 1 Marti, Adrian 1 Miller, Dale Allen 1 Monks, Kenneth G. 1 Mosteghanemi, M’hamed 1 Mu, Shin-Cheng 1 Nevzorova, Ol’ga Avenirovna 1 Nie, Pengyu 1 Nieva, Susana 1 Ogata, Kazuhiro 1 Oliveira, José Nuno 1 Oripov, Akbar 1 Palmskog, Karl 1 Paulson, Lawrence Charles ...and 43 more Authors all top 5 Cited in 20 Serials 11 Journal of Automated Reasoning 4 MSCS. Mathematical Structures in Computer Science 3 Theoretical Computer Science 2 Journal of Symbolic Computation 2 Information and Computation 2 Mathematics in Computer Science 1 The Mathematical Intelligencer 1 Formal Aspects of Computing 1 AI Communications 1 Annals of Mathematics and Artificial Intelligence 1 Séminaire Lotharingien de Combinatoire 1 Soft Computing 1 Lobachevskii Journal of Mathematics 1 Computer Languages, Systems & Structures 1 ACM Transactions on Computational Logic 1 Mathematical Biosciences and Engineering 1 Logica Universalis 1 Logical Methods in Computer Science 1 Journal of Formalized Reasoning 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 9 Fields 89 Computer science (68-XX) 33 Mathematical logic and foundations (03-XX) 3 General and overarching topics; collections (00-XX) 2 Combinatorics (05-XX) 1 History and biography (01-XX) 1 Number theory (11-XX) 1 Special functions (33-XX) 1 Numerical analysis (65-XX) 1 Operations research, mathematical programming (90-XX) Citations by Year