Florian Rabe

ORCID

Publication Activity (10 Years)

Years Active: 2006-2024
Publications (10 Years): 52

Top Venues

Publications

Florian Rabe, Claudio Sacerdoti Coen
Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. CoRR (2024)
Florian Rabe
A Logical Framework Perspective on Conservativity. CICM (2024)
Andrej Bauer, Katja Bercic, Florian Rabe, Nicolas M. Thiéry, Jure Taslak
Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401). Dagstuhl Reports 13 (10) (2023)
Colin Rothgang, Florian Rabe, Christoph Benzmüller
Theorem Proving in Dependently-Typed Higher-Order Logic - Extended Preprint. CoRR (2023)
Colin Rothgang, Florian Rabe, Christoph Benzmüller
Theorem Proving in Dependently-Typed Higher-Order Logic. CADE (2023)
Florian Rabe, Stephen M. Watt
Extracting Theory Graphs from Aldor Libraries. CICM (2023)
Florian Rabe, Franziska Weber
Morphism Equality in Theory Graphs. CICM (2023)
Michael Kohlhase, Florian Rabe
Experiences from Exporting Major Proof Assistant Libraries. J. Autom. Reason. 65 (8) (2021)
Florian Rabe
A Language with Type-Dependent Equality. CICM (2021)
Florian Rabe, Navid Roux
Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style. LFMTP (2021)
Colin Rothgang, Artur Kornilowicz, Florian Rabe
A New Export of the Mizar Mathematical Library. CICM (2021)
Cezary Kaliszyk, Florian Rabe
A Survey of Languages for Formalizing Mathematics. CICM (2020)
Michael Kohlhase, Florian Rabe, Makarius Wenzel
Making Isabelle Content Accessible in Knowledge Representation Formats. CoRR (2020)
Katja Bercic, Michael Kohlhase, Florian Rabe
(Deep) FAIR mathematics. it Inf. Technol. 62 (1) (2020)
Katja Bercic, Michael Kohlhase, Florian Rabe
Towards a Heterogeneous Query Language for Mathematical Knowledge. CICM (2020)
Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer
Logic-Independent Proof Search in Logical Frameworks - (Short Paper). IJCAR (1) (2020)
Richard Marcus, Michael Kohlhase, Florian Rabe
TGView3D: A System for 3-Dimensional Visualization of Theory Graphs. CICM (2020)
Cezary Kaliszyk, Florian Rabe
A Survey of Languages for Formalizing Mathematics. CoRR (2020)
Michael Kohlhase, Florian Rabe
Experiences from Exporting Major Proof Assistant Libraries. CoRR (2020)
Dennis Müller, Florian Rabe, Colin Rothgang, Michael Kohlhase
Representing Structural Language Features in Formal Meta-languages. CICM (2020)
Katja Bercic, Jacques Carette, William M. Farmer, Michael Kohlhase, Dennis Müller, Florian Rabe, Yasmine Sharoda
The Space of Mathematical Software Systems - A Survey of Paradigmatic Systems. CoRR (2020)
Navid Roux, Florian Rabe
Structure-Preserving Diagram Operators. WADT (2020)
Florian Rabe, Yasmine Sharoda
Diagram Combinators in MMT. CICM (2019)
Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe
Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal. CoRR (2019)
Andrea Condoluci, Michael Kohlhase, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen, Makarius Wenzel
Relational Data Across Mathematical Libraries. CICM (2019)
Kai Amann, Michael Kohlhase, Florian Rabe, Tom Wiesing
Integrating Semantic Mathematical Documents and Dynamic Notebooks. CICM (2019)
Florian Rabe
MMTTeX: Connecting Content and Narration-Oriented Document Formats. CICM (2019)
Richard Bird, Florian Rabe
How to Calculate with Nondeterministic Functions. MPC (2019)
Katja Bercic, Michael Kohlhase, Florian Rabe
Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation. CICM (2019)
Michael Kohlhase, Florian Rabe, Makarius Wenzel
Making Isabelle Content Accessible in Knowledge Representation Formats. TYPES (2019)
Dennis Müller, Florian Rabe
Rapid Prototyping Formal Systems in MMT: 5 Case Studies. LFMTP@LICS (2019)
Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen
The Coq Library as a Theory Graph. CICM (2019)
Richard Marcus, Michael Kohlhase, Florian Rabe
TGView3D System Description: 3-Dimensional Visualization of Theory Graphs. CoRR (2019)
Dennis Müller, Florian Rabe, Michael Kohlhase
Theories as Types. IJCAR (2018)
Florian Rabe, Dennis Müller
Structuring Theories with Implicit Morphisms. WADT (2018)
Dennis Müller, Michael Kohlhase, Florian Rabe
Automatically Finding Theory Morphisms for Knowledge Management. CICM (2018)
Florian Rabe
A Modular Type Reconstruction Algorithm. ACM Trans. Comput. Log. 19 (4) (2018)
Michael Kohlhase, Luca De Feo, Dennis Müller, Markus Pfeiffer, Florian Rabe, Nicolas M. Thiéry, Victor Vasilyev, Tom Wiesing
Knowledge-Based Interoperability for Mathematical Software Systems. MACIS (2017)
Florian Rabe
Morphism axioms. Theor. Comput. Sci. 691 (2017)
Michael Kohlhase, Dennis Müller, Sam Owre, Florian Rabe
Making PVS Accessible to Generic Services by Interpretation in a Universal Format. ITP (2017)
Dennis Müller, Colin Rothgang, Yufei Liu, Florian Rabe
Alignment-based Translations Across Formal Systems Using Interface Theories. PxTP (2017)
Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe
Classification of Alignments Between Concepts of Formal Mathematical Systems. CICM (2017)
Till Mossakowski, Florian Rabe, Mihai Codescu
Canonical Selection of Colimits. CoRR (2017)
Florian Rabe
How to identify, translate and combine logics? J. Log. Comput. 27 (6) (2017)
Tom Wiesing, Michael Kohlhase, Florian Rabe
Virtual Theories - A Uniform Interface to Mathematical Knowledge Bases. MACIS (2017)
Cezary Kaliszyk, Michael Kohlhase, Dennis Müller, Florian Rabe
A Standard for Aligning Mathematical Concepts. FM4M/MathUI/ThEdu/DP/WIP@CIKM (2016)
Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe
Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Reports 6 (10) (2016)
Paul-Olivier Dehaye, Mihnea Iancu, Michael Kohlhase, Alexander Konovalov, Samuel Lelièvre, Dennis Müller, Markus Pfeiffer, Florian Rabe, Nicolas M. Thiéry, Tom Wiesing
Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach. CICM (2016)
Michael Kohlhase, Florian Rabe
QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge. J. Formaliz. Reason. 9 (1) (2016)
Till Mossakowski, Florian Rabe, Mihai Codescu
Canonical Selection of Colimits. WADT (2016)
Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe
TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. PAAR@IJCAR (2016)
Florian Rabe
The Future of Logic: Foundation-Independence. Logica Universalis 10 (1) (2016)
Florian Rabe
Generic Literals. CICM (2015)
Feryal Fulya Horozal, Florian Rabe
Formal Logic Definitions for Interchange Languages. CICM (2015)
Florian Rabe
Lax Theory Morphisms. ACM Trans. Comput. Log. 17 (1) (2015)
Feryal Fulya Horozal, Florian Rabe, Michael Kohlhase
Flexary Operators for Formalized Mathematics. CICM (2014)
Florian Rabe
MMT Objects. CICM Workshops (2014)
Florian Rabe
A Logic-Independent IDE. UITP (2014)
Cezary Kaliszyk, Florian Rabe
Towards Knowledge Management for HOL Light. CICM (2014)
Mihnea Iancu, Michael Kohlhase, Florian Rabe, Josef Urban
The Mizar Mathematical Library in OMDoc: Translation and Applications. J. Autom. Reason. 50 (2) (2013)
Florian Rabe
A logical framework combining model and proof theory. Math. Struct. Comput. Sci. 23 (5) (2013)
Michael Kohlhase, Felix Mance, Florian Rabe
A Universal Machine for Biform Theory Graphs. CoRR (2013)
Michael Kohlhase, Felix Mance, Florian Rabe
A Universal Machine for Biform Theory Graphs. MKM/Calculemus/DML (2013)
Florian Rabe, Kristina Sojakova
Logical relations for a logical framework. ACM Trans. Comput. Log. 14 (4) (2013)
Florian Rabe
The MMT API: A Generic MKM System. MKM/Calculemus/DML (2013)
Mihnea Iancu, Felix Mance, Florian Rabe
The Scala-REPL + MMT as a lightweight mathematical user interface. CICM Workshops (2013)
Florian Rabe
The MMT API: A Generic MKM System. CoRR (2013)
Florian Rabe, Michael Kohlhase
A scalable module system. Inf. Comput. 230 (2013)
Michael Kohlhase, Florian Rabe
Semantics of OpenMath and MathML3. Math. Comput. Sci. 6 (3) (2012)
Florian Rabe
A Query Language for Formal Mathematical Libraries. AISC/MKM/Calculemus (2012)
Mihai Codescu, Feryal Fulya Horozal, Aivaras Jakubauskas, Till Mossakowski, Florian Rabe
Compiling Logics. WADT (2012)
Mihnea Iancu, Florian Rabe
Management of Change in Declarative Languages. AISC/MKM/Calculemus (2012)
Florian Rabe
A Query Language for Formal Mathematical Libraries CoRR (2012)
Feryal Fulya Horozal, Michael Kohlhase, Florian Rabe
Extending MKM Formats at the Statement Level. AISC/MKM/Calculemus (2012)
Mihai Codescu, Feryal Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe
Project Abstract: Logic Atlas and Integrator (LATIN). Calculemus/MKM (2011)
Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen
A Foundational View on Integration Problems. Calculemus/MKM (2011)
Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen
A Foundational View on Integration Problems CoRR (2011)
Steven Awodey, Florian Rabe
Kripke Semantics for Martin-Löf's Extensional Type Theory Log. Methods Comput. Sci. 7 (3) (2011)
Feryal Fulya Horozal, Florian Rabe
Representing model theory in a type-theoretical logical framework. Theor. Comput. Sci. 412 (37) (2011)
Florian Rabe, Michael Kohlhase
A Scalable Module System CoRR (2011)
Mihnea Iancu, Florian Rabe
Formalising foundations of mathematics. Math. Struct. Comput. Sci. 21 (4) (2011)
Feryal Fulya Horozal, Alin Iacob, Constantin Jucovschi, Michael Kohlhase, Florian Rabe
Combining Source, Content, Presentation, Narration, and Relational Representation. Calculemus/MKM (2011)
Michael Kohlhase, Florian Rabe, Vyacheslav Zholudev
Towards MKM in the Large: Modular Representation and Scalable Software Architecture CoRR (2010)
Catalin David, Michael Kohlhase, Christoph Lange, Florian Rabe, Nikita Zhiltsov, Vyacheslav Zholudev
Publishing Math Lecture Notes as Linked Data. ESWC (2) (2010)
Mihai Codescu, Feryal Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe
A Proof Theoretic Interpretation of Model Theoretic Hiding. WADT (2010)
Michael Kohlhase, Florian Rabe, Vyacheslav Zholudev
Towards MKM in the Large: Modular Representation and Scalable Software Architecture. AISC/MKM/Calculemus (2010)
Mihai Codescu, Feryal Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe, Kristina Sojakova
Towards Logical Frameworks in the Heterogeneous Tool Set Hets. WADT (2010)
Florian Rabe
Representing Isabelle in LF LFMTP (2010)
Catalin David, Michael Kohlhase, Christoph Lange, Florian Rabe, Nikita Zhiltsov, Vyacheslav Zholudev
Publishing Math Lecture Notes as Linked Data CoRR (2010)
Feryal Fulya Horozal, Florian Rabe
Representing Model Theory in a Type-Theoretical Logical Framework. LSFA (2009)
Florian Rabe, Petr Pudlák, Geoff Sutcliffe, Weina Shen
Solving the $100 modal logic challenge. J. Appl. Log. 7 (1) (2009)
Jana Giceva, Christoph Lange, Florian Rabe
Integrating Web Services into Active Mathematical Documents. Calculemus/MKM (2009)
Florian Rabe, Carsten Schürmann
A practical module system for LF. LFMTP (2009)
Steven Awodey, Florian Rabe
Kripke Semantics for Martin-Löf's Extensional Type Theory. TLCA (2009)
Christoph Benzmüller, Florian Rabe, Carsten Schürmann, Geoff Sutcliffe
Evaluation of Systems for Higher-order Logic (ESHOL). PAAR/ESHOL (2008)
Michael Kohlhase, Christine Müller, Florian Rabe
Notations for Living Mathematical Documents. AISC/MKM/Calculemus (2008)
Christoph Lange, Sean McLaughlin, Florian Rabe
Flyspeck in a Semantic Wiki. SemWiki (2008)
Kristina Sojakova, Florian Rabe
Translating a Dependently-Typed Logic to First-Order Logic. WADT (2008)
Florian Rabe, Michael Kohlhase
An Exchange Format for Modular Knowledge. LPAR Workshops (2008)
Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe
THF0 - The Core of the TPTP Language for Higher-Order Logic. IJCAR (2008)

Florian Rabe.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Florian Rabe