×
Author ID: rabe.florian Recent zbMATH articles by "Rabe, Florian"
Published as: Rabe, Florian
Homepage: https://kwarc.info/people/frabe/
External Links: MGP · ORCID · dblp

Publications by Year

Citations contained in zbMATH Open

57 Publications have been cited 274 times in 113 Documents Cited by Year
A scalable module system. Zbl 1358.68283
Rabe, Florian; Kohlhase, Michael
37
2013
The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375
Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef
19
2013
Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
18
2011
The MMT API: a generic MKM system. Zbl 1390.68626
Rabe, Florian
18
2013
Formalising foundations of mathematics. Zbl 1242.03031
Iancu, Mihnea; Rabe, Florian
12
2011
How to identify, translate and combine logics? Zbl 1444.03121
Rabe, Florian
11
2017
Representing model theory in a type-theoretical logical framework. Zbl 1236.03027
Horozal, Fulya; Rabe, Florian
9
2011
A logical framework combining model and proof theory. Zbl 1326.03082
Rabe, Florian
8
2013
THF0 – the core of the TPTP language for higher-order logic. Zbl 1165.68447
Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff
8
2008
Towards logical frameworks in the heterogeneous tool set Hets. Zbl 1278.68286
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina
8
2012
Flexary operators for formalized mathematics. Zbl 1304.68171
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael
7
2014
Extending MKM formats at the statement level. Zbl 1278.68293
Horozal, Fulya; Kohlhase, Michael; Rabe, Florian
7
2012
Towards MKM in the large: modular representation and scalable software architecture. Zbl 1278.68297
Kohlhase, Michael; Rabe, Florian; Zholudev, Vyacheslav
7
2010
Notations for living mathematical documents. Zbl 1166.00304
Kohlhase, Michael; Müller, Christine; Rabe, Florian
7
2008
A foundational view on integration problems. Zbl 1278.68289
Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio
6
2011
A survey of languages for formalizing mathematics. Zbl 1455.68257
Kaliszyk, Cezary; Rabe, Florian
6
2020
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
5
2017
Towards knowledge management for HOL Light. Zbl 1304.68158
Kaliszyk, Cezary; Rabe, Florian
5
2014
Integrating web services into active mathematical documents. Zbl 1247.68314
Giceva, Jana; Lange, Christoph; Rabe, Florian
5
2009
Generic literals. Zbl 1417.68216
Rabe, Florian
4
2015
A modular type reconstruction algorithm. Zbl 1407.68440
Rabe, Florian
4
2018
Representing structural language features in formal meta-languages. Zbl 1455.68268
Müller, Dennis; Rabe, Florian; Rothgang, Colin; Kohlhase, Michael
4
2020
QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343
Kohlhase, Michael; Rabe, Florian
4
2016
Logical relations for a logical framework. Zbl 1353.68252
Rabe, Florian; Sojakova, Kristina
3
2013
Theories as types. Zbl 1511.68340
Müller, Dennis; Rabe, Florian; Kohlhase, Michael
3
2018
A query language for formal mathematical libraries. Zbl 1359.68272
Rabe, Florian
3
2012
The Coq library as a theory graph. Zbl 1428.68344
Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio
3
2019
First-order logic with dependent types. Zbl 1222.03016
Rabe, Florian
3
2006
Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Zbl 1316.68015
2
2015
The future of logic: foundation-independence. Zbl 1436.03179
Rabe, Florian
2
2016
Interoperability in the OpenDreamKit project: the math-in-the-middle approach. Zbl 1344.68268
Dehaye, 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 1237.03007
Awodey, Steve; Rabe, Florian
2
2011
Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 1497.68550
Wiesing, Tom; Kohlhase, Michael; Rabe, Florian
2
2017
Kripke semantics for Martin-Löf’s extensional type theory. Zbl 1246.03022
Awodey, Steve; Rabe, Florian
2
2009
A universal machine for biform theory graphs. Zbl 1278.68267
Kohlhase, Michael; Mance, Felix; Rabe, Florian
2
2013
Making PVS accessible to generic services by interpretation in a universal format. Zbl 1484.68311
Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian
2
2017
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
Relational data across mathematical libraries. Zbl 1428.68352
Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius
2
2019
How to calculate with nondeterministic functions. Zbl 1434.68078
Bird, Richard; Rabe, Florian
2
2019
Formal logic definitions for interchange languages. Zbl 1417.68206
Horozal, Fulya; Rabe, Florian
1
2015
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.03061
Rabe, Florian
1
2015
Morphism axioms. Zbl 1373.03132
Rabe, Florian
1
2017
Compiling logics. Zbl 1394.68071
Codescu, Mihai; Horozal, Fulya; Jakubauskas, Aivaras; Mossakowski, Till; Rabe, Florian
1
2013
Representing model theory in a type-theoretical logical framework. Zbl 1291.03068
Horozal, Fulya; Rabe, Florian
1
2009
Automatically finding theory morphisms for knowledge management. Zbl 1417.68211
Müller, Dennis; Kohlhase, Michael; Rabe, Florian
1
2018
A proof theoretic interpretation of model theoretic hiding. Zbl 1278.68202
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
1
2012
Combining source, content, presentation, narration, and relational representation. Zbl 1278.68292
Horozal, Fulya; Iacob, Alin; Jucovschi, Constantin; Kohlhase, Michael; Rabe, Florian
1
2011
Semantics of OpenMath and MathML3. Zbl 1271.68221
Kohlhase, Michael; Rabe, Florian
1
2012
Experiences from exporting major proof assistant libraries. Zbl 07461271
Kohlhase, Michael; Rabe, Florian
1
2021
Towards a heterogeneous query language for mathematical knowledge. Zbl 1455.68264
Berčič, Katja; Kohlhase, Michael; Rabe, Florian
1
2020
TGView3D: a system for 3-dimensional visualization of theory graphs. Zbl 1455.68267
Marcus, Richard; Kohlhase, Michael; Rabe, Florian
1
2020
Canonical selection of colimits. Zbl 1496.68203
Mossakowski, Till; Rabe, Florian; Codescu, Mihai
1
2017
Towards a unified mathematical data infrastructure: database and interface generation. Zbl 1428.68356
Berčič, Katja; Kohlhase, Michael; Rabe, Florian
1
2019
Diagram combinators in MMT. Zbl 1428.68353
Rabe, Florian; Sharoda, Yasmine
1
2019
Solving the $100 modal logic challenge. Zbl 1161.03302
Rabe, Florian; Pudlák, Petr; Sutcliffe, Geoff; Shen, Weina
1
2009
Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge. Zbl 1493.68391
Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian
1
2021
Experiences from exporting major proof assistant libraries. Zbl 07461271
Kohlhase, Michael; Rabe, Florian
1
2021
Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge. Zbl 1493.68391
Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian
1
2021
A survey of languages for formalizing mathematics. Zbl 1455.68257
Kaliszyk, Cezary; Rabe, Florian
6
2020
Representing structural language features in formal meta-languages. Zbl 1455.68268
Müller, Dennis; Rabe, Florian; Rothgang, Colin; Kohlhase, Michael
4
2020
Towards a heterogeneous query language for mathematical knowledge. Zbl 1455.68264
Berčič, Katja; Kohlhase, Michael; Rabe, Florian
1
2020
TGView3D: a system for 3-dimensional visualization of theory graphs. Zbl 1455.68267
Marcus, Richard; Kohlhase, Michael; Rabe, Florian
1
2020
The Coq library as a theory graph. Zbl 1428.68344
Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio
3
2019
Relational data across mathematical libraries. Zbl 1428.68352
Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius
2
2019
How to calculate with nondeterministic functions. Zbl 1434.68078
Bird, Richard; Rabe, Florian
2
2019
Towards a unified mathematical data infrastructure: database and interface generation. Zbl 1428.68356
Berčič, Katja; Kohlhase, Michael; Rabe, Florian
1
2019
Diagram combinators in MMT. Zbl 1428.68353
Rabe, Florian; Sharoda, Yasmine
1
2019
A modular type reconstruction algorithm. Zbl 1407.68440
Rabe, Florian
4
2018
Theories as types. Zbl 1511.68340
Müller, Dennis; Rabe, Florian; Kohlhase, Michael
3
2018
Automatically finding theory morphisms for knowledge management. Zbl 1417.68211
Müller, Dennis; Kohlhase, Michael; Rabe, Florian
1
2018
How to identify, translate and combine logics? Zbl 1444.03121
Rabe, Florian
11
2017
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
5
2017
Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 1497.68550
Wiesing, Tom; Kohlhase, Michael; Rabe, Florian
2
2017
Making PVS accessible to generic services by interpretation in a universal format. Zbl 1484.68311
Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian
2
2017
Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Zbl 1364.68010
1
2017
Morphism axioms. Zbl 1373.03132
Rabe, Florian
1
2017
Canonical selection of colimits. Zbl 1496.68203
Mossakowski, Till; Rabe, Florian; Codescu, Mihai
1
2017
QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343
Kohlhase, Michael; Rabe, Florian
4
2016
The future of logic: foundation-independence. Zbl 1436.03179
Rabe, Florian
2
2016
Interoperability in the OpenDreamKit project: the math-in-the-middle approach. Zbl 1344.68268
Dehaye, 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
Generic literals. Zbl 1417.68216
Rabe, Florian
4
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.68206
Horozal, Fulya; Rabe, Florian
1
2015
Lax theory morphisms. Zbl 1367.03061
Rabe, Florian
1
2015
Flexary operators for formalized mathematics. Zbl 1304.68171
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael
7
2014
Towards knowledge management for HOL Light. Zbl 1304.68158
Kaliszyk, Cezary; Rabe, Florian
5
2014
A scalable module system. Zbl 1358.68283
Rabe, Florian; Kohlhase, Michael
37
2013
The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375
Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef
19
2013
The MMT API: a generic MKM system. Zbl 1390.68626
Rabe, Florian
18
2013
A logical framework combining model and proof theory. Zbl 1326.03082
Rabe, Florian
8
2013
Logical relations for a logical framework. Zbl 1353.68252
Rabe, Florian; Sojakova, Kristina
3
2013
A universal machine for biform theory graphs. Zbl 1278.68267
Kohlhase, Michael; Mance, Felix; Rabe, Florian
2
2013
Compiling logics. Zbl 1394.68071
Codescu, Mihai; Horozal, Fulya; Jakubauskas, Aivaras; Mossakowski, Till; Rabe, Florian
1
2013
Towards logical frameworks in the heterogeneous tool set Hets. Zbl 1278.68286
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina
8
2012
Extending MKM formats at the statement level. Zbl 1278.68293
Horozal, Fulya; Kohlhase, Michael; Rabe, Florian
7
2012
A query language for formal mathematical libraries. Zbl 1359.68272
Rabe, Florian
3
2012
A proof theoretic interpretation of model theoretic hiding. Zbl 1278.68202
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
1
2012
Semantics of OpenMath and MathML3. Zbl 1271.68221
Kohlhase, Michael; Rabe, Florian
1
2012
Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
18
2011
Formalising foundations of mathematics. Zbl 1242.03031
Iancu, Mihnea; Rabe, Florian
12
2011
Representing model theory in a type-theoretical logical framework. Zbl 1236.03027
Horozal, Fulya; Rabe, Florian
9
2011
A foundational view on integration problems. Zbl 1278.68289
Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio
6
2011
Kripke semantics for Martin-Löf’s extensional type theory. Zbl 1237.03007
Awodey, 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
Combining source, content, presentation, narration, and relational representation. Zbl 1278.68292
Horozal, Fulya; Iacob, Alin; Jucovschi, Constantin; Kohlhase, Michael; Rabe, Florian
1
2011
Towards MKM in the large: modular representation and scalable software architecture. Zbl 1278.68297
Kohlhase, Michael; Rabe, Florian; Zholudev, Vyacheslav
7
2010
Integrating web services into active mathematical documents. Zbl 1247.68314
Giceva, Jana; Lange, Christoph; Rabe, Florian
5
2009
Kripke semantics for Martin-Löf’s extensional type theory. Zbl 1246.03022
Awodey, Steve; Rabe, Florian
2
2009
Representing model theory in a type-theoretical logical framework. Zbl 1291.03068
Horozal, Fulya; Rabe, Florian
1
2009
Solving the $100 modal logic challenge. Zbl 1161.03302
Rabe, Florian; Pudlák, Petr; Sutcliffe, Geoff; Shen, Weina
1
2009
THF0 – the core of the TPTP language for higher-order logic. Zbl 1165.68447
Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff
8
2008
Notations for living mathematical documents. Zbl 1166.00304
Kohlhase, Michael; Müller, Christine; Rabe, Florian
7
2008
First-order logic with dependent types. Zbl 1222.03016
Rabe, Florian
3
2006
all top 5

Cited by 158 Authors

33 Rabe, Florian
30 Kohlhase, Michael
10 Kaliszyk, Cezary
8 Horozal, Fulya
7 Müller, Dennis
7 Pąk, Karol
6 Iancu, Mihnea
6 Korniłowicz, Artur
5 Benzmüller, Christoph Ewald
5 Mossakowski, Till
4 Carette, Jacques
4 Codescu, Mihai
4 Farmer, William M.
4 Gauthier, Thibault
4 Kohlhase, Andrea
4 Naumowicz, Adam
4 Sacerdoti Coen, Claudio
4 Sutcliffe, Geoff
3 Brown, Chad Edward
3 Foster, Simon
3 Grabowski, Adam
3 Kirillovich, Aleksandr Vital’evich
3 Lipachëv, E. K.
3 Nevzorova, Ol’ga Avenirovna
3 Urban, Josef
3 Wiesing, Tom
2 Bancerek, Grzegorz
2 Bauer, Andrej
2 Berčič, Katja
2 Byliński, Czesław
2 Cauderlier, Raphaël
2 Dundua, Besik
2 Elizarov, A. M.
2 Guidi, Ferruccio
2 Jucovschi, Constantin
2 Kutsia, Temur
2 Lange, Christoph
2 Matuszewski, Roman
2 Paulson, Lawrence Charles
2 Sojakova, Kristina
2 Sperber, Wolfram
2 Theiss, Frank
2 Wenzel, Makarius
2 Zeyda, Frank
1 Adams, Robin
1 Alessi, Fabio
1 Auer, Sören
1 Awodey, Steve
1 Barbosa, Luís Soares
1 Baumeister, Hubert
1 Belo, João Filipe
1 Bettaz, Mohamed
1 Burel, Guillaume
1 Bury, Guillaume
1 Carter, Nathan C.
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 Dubois, Catherine
1 Dunne, Ciarán
1 Fietzke, Arnaud
1 Freitas, Leo
1 Fürsich, Michael
1 Furushima, Hideharu
1 Futatsugi, Kokichi
1 Giceva, Jana
1 Ginev, Deyan
1 Gligorić, Miloš V.
1 Halmagrand, Pierre
1 Haselwarter, Philipp G.
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 Koepke, Peter
1 Konovalov, Olexandr
1 Koprucki, Thomas
1 Kutz, Oliver
1 Lelièvre, Samuel
1 Lenisa, Marina
1 Lewis, Robert Y.
1 Li, Junyi Jessy
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.
...and 58 more Authors

Citations by Year