First-Order Logic with Dependent Types. - Florian Rabe 001 (IJCAR, 2006)

An Institutional View on Categorical Logic. - Joseph A. Goguen; Till Mossakowski; Valeria de Paiva; Florian Rabe 001; Lutz Schröder (Int. J. Softw. Informatics, 2007)

Representing logics and logic translations. - Florian Rabe 001 (2008)

Notations for Living Mathematical Documents. - Michael Kohlhase; Christine Müller; Florian Rabe 001 (AISC/MKM/Calculemus, 2008)

THF0 - The Core of the TPTP Language for Higher-Order Logic. - Christoph Benzmüller; Florian Rabe 001; Geoff Sutcliffe (IJCAR, 2008)

Evaluation of Systems for Higher-order Logic (ESHOL). - Christoph Benzmüller; Florian Rabe 001; Carsten Schürmann; Geoff Sutcliffe (PAAR/ESHOL, 2008)

Repräsentation von Logiken und Logik-Übersetzungen [Representing Logics and Logic Translations]. - Florian Rabe 001 (Ausgezeichnete Informatikdissertationen, 2008)

An Exchange Format for Modular Knowledge. - Florian Rabe 001; Michael Kohlhase (LPAR Workshops, 2008)

Flyspeck in a Semantic Wiki. - Christoph Lange 002; Sean McLaughlin; Florian Rabe 001 (SemWiki, 2008)

Translating a Dependently-Typed Logic to First-Order Logic. - Kristina Sojakova; Florian Rabe 001 (WADT, 2008)

A practical module system for LF. - Florian Rabe 001; Carsten Schürmann (LFMTP, 2009)

Integrating Web Services into Active Mathematical Documents. - Jana Giceva; Christoph Lange 002; Florian Rabe 001 (Calculemus/MKM, 2009)

Solving the $100 modal logic challenge. - Florian Rabe 001; Petr Pudlák; Geoff Sutcliffe; Weina Shen (J. Appl. Log., 2009)

Towards MKM in the Large: Modular Representation and Scalable Software Architecture. - Michael Kohlhase; Florian Rabe 001; Vyacheslav Zholudev (AISC/MKM/Calculemus, 2010)

Publishing Math Lecture Notes as Linked Data. - Catalin David; Michael Kohlhase; Christoph Lange 002; Florian Rabe 001; Nikita Zhiltsov; Vyacheslav Zholudev (ESWC (2), 2010)

A Proof Theoretic Interpretation of Model Theoretic Hiding. - Mihai Codescu; Feryal Fulya Horozal; Michael Kohlhase; Till Mossakowski; Florian Rabe 001 (WADT, 2010)

Towards Logical Frameworks in the Heterogeneous Tool Set Hets. - Mihai Codescu; Feryal Fulya Horozal; Michael Kohlhase; Till Mossakowski; Florian Rabe 001; Kristina Sojakova (WADT, 2010)

Representing Isabelle in LF - Florian Rabe 001 (LFMTP, 2010)

Project Abstract: Logic Atlas and Integrator (LATIN). - Mihai Codescu; Feryal Fulya Horozal; Michael Kohlhase; Till Mossakowski; Florian Rabe 001 (Calculemus/MKM, 2011)

Combining Source, Content, Presentation, Narration, and Relational Representation. - Feryal Fulya Horozal; Alin Iacob; Constantin Jucovschi; Michael Kohlhase; Florian Rabe 001 (Calculemus/MKM, 2011)

A Foundational View on Integration Problems. - Florian Rabe 001; Michael Kohlhase; Claudio Sacerdoti Coen (Calculemus/MKM, 2011)

Kripke Semantics for Martin-Löf's Extensional Type Theory - Steven Awodey; Florian Rabe 001 (Log. Methods Comput. Sci., 2011)

Formalising foundations of mathematics. - Mihnea Iancu; Florian Rabe 001 (Math. Struct. Comput. Sci., 2011)

Representing model theory in a type-theoretical logical framework. - Feryal Fulya Horozal; Florian Rabe 001 (Theor. Comput. Sci., 2011)

Extending MKM Formats at the Statement Level. - Feryal Fulya Horozal; Michael Kohlhase; Florian Rabe 001 (AISC/MKM/Calculemus, 2012)

Management of Change in Declarative Languages. - Mihnea Iancu; Florian Rabe 001 (AISC/MKM/Calculemus, 2012)

A Query Language for Formal Mathematical Libraries. - Florian Rabe 001 (AISC/MKM/Calculemus, 2012)

Compiling Logics. - Mihai Codescu; Feryal Fulya Horozal; Aivaras Jakubauskas; Till Mossakowski; Florian Rabe 001 (WADT, 2012)

Semantics of OpenMath and MathML3. - Michael Kohlhase; Florian Rabe 001 (Math. Comput. Sci., 2012)

The Scala-REPL + MMT as a lightweight mathematical user interface. - Mihnea Iancu; Felix Mance; Florian Rabe 001 (CICM Workshops, 2013)

A Universal Machine for Biform Theory Graphs. - Michael Kohlhase; Felix Mance; Florian Rabe 001 (MKM/Calculemus/DML, 2013)

The MMT API: A Generic MKM System. - Florian Rabe 001 (MKM/Calculemus/DML, 2013)

A scalable module system. - Florian Rabe 001; Michael Kohlhase (Inf. Comput., 2013)

The Mizar Mathematical Library in OMDoc: Translation and Applications. - Mihnea Iancu; Michael Kohlhase; Florian Rabe 001; Josef Urban (J. Autom. Reason., 2013)

A logical framework combining model and proof theory. - Florian Rabe 001 (Math. Struct. Comput. Sci., 2013)

Logical relations for a logical framework. - Florian Rabe 001; Kristina Sojakova (ACM Trans. Comput. Log., 2013)

Flexary Operators for Formalized Mathematics. - Feryal Fulya Horozal; Florian Rabe 001; Michael Kohlhase (CICM, 2014)

Towards Knowledge Management for HOL Light. - Cezary Kaliszyk; Florian Rabe 001 (CICM, 2014)

MMT Objects. - Florian Rabe 001 (CICM Workshops, 2014)

A Logic-Independent IDE. - Florian Rabe 001 (UITP, 2014)

Formal Logic Definitions for Interchange Languages. - Feryal Fulya Horozal; Florian Rabe 001 (CICM, 2015)

Generic Literals. - Florian Rabe 001 (CICM, 2015)

Lax Theory Morphisms. - Florian Rabe 001 (ACM Trans. Comput. Log., 2015)

TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. - Cezary Kaliszyk; Geoff Sutcliffe; Florian Rabe 001 (PAAR@IJCAR, 2016)

A Standard for Aligning Mathematical Concepts. - Cezary Kaliszyk; Michael Kohlhase; Dennis Müller 001; Florian Rabe 001 (FM4M/MathUI/ThEdu/DP/WIP@CIKM, 2016)

Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach. - Paul-Olivier Dehaye; Mihnea Iancu; Michael Kohlhase; Alexander Konovalov 001; Samuel Lelièvre; Dennis Müller 001; Markus Pfeiffer; Florian Rabe 001; Nicolas M. Thiéry; Tom Wiesing (CICM, 2016)

Canonical Selection of Colimits. - Till Mossakowski; Florian Rabe 001; Mihai Codescu (WADT, 2016)

Universality of Proofs (Dagstuhl Seminar 16421). - Gilles Dowek; Catherine Dubois; Brigitte Pientka; Florian Rabe 001 (Dagstuhl Reports, 2016)

QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge. - Michael Kohlhase; Florian Rabe 001 (J. Formaliz. Reason., 2016)

The Future of Logic: Foundation-Independence. - Florian Rabe 001 (Logica Universalis, 2016)

Making PVS Accessible to Generic Services by Interpretation in a Universal Format. - Michael Kohlhase; Dennis Müller 001; Sam Owre; Florian Rabe 001 (ITP, 2017)

Knowledge-Based Interoperability for Mathematical Software Systems. - Michael Kohlhase; Luca De Feo; Dennis Müller 001; Markus Pfeiffer; Florian Rabe 001; Nicolas M. Thiéry; Victor Vasilyev; Tom Wiesing (MACIS, 2017)

Virtual Theories - A Uniform Interface to Mathematical Knowledge Bases. - Tom Wiesing; Michael Kohlhase; Florian Rabe 001 (MACIS, 2017)

Classification of Alignments Between Concepts of Formal Mathematical Systems. - Dennis Müller 001; Thibault Gauthier; Cezary Kaliszyk; Michael Kohlhase; Florian Rabe 001 (CICM, 2017)

Alignment-based Translations Across Formal Systems Using Interface Theories. - Dennis Müller 001; Colin Rothgang; Yufei Liu; Florian Rabe 001 (PxTP, 2017)

How to identify, translate and combine logics? - Florian Rabe 001 (J. Log. Comput., 2017)

Morphism axioms. - Florian Rabe 001 (Theor. Comput. Sci., 2017)

Theories as Types. - Dennis Müller 001; Florian Rabe 001; Michael Kohlhase (IJCAR, 2018)

Automatically Finding Theory Morphisms for Knowledge Management. - Dennis Müller 001; Michael Kohlhase; Florian Rabe 001 (CICM, 2018)

Structuring Theories with Implicit Morphisms. - Florian Rabe 001; Dennis Müller 001 (WADT, 2018)

A Modular Type Reconstruction Algorithm. - Florian Rabe 001 (ACM Trans. Comput. Log., 2018)

The Coq Library as a Theory Graph. - Dennis Müller 001; Florian Rabe 001; Claudio Sacerdoti Coen (CICM, 2019)

Integrating Semantic Mathematical Documents and Dynamic Notebooks. - Kai Amann; Michael Kohlhase; Florian Rabe 001; Tom Wiesing (CICM, 2019)

Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation. - Katja Bercic; Michael Kohlhase; Florian Rabe 001 (CICM, 2019)

Relational Data Across Mathematical Libraries. - Andrea Condoluci; Michael Kohlhase; Dennis Müller 001; Florian Rabe 001; Claudio Sacerdoti Coen; Makarius Wenzel (CICM, 2019)

MMTTeX: Connecting Content and Narration-Oriented Document Formats. - Florian Rabe 001 (CICM, 2019)

Diagram Combinators in MMT. - Florian Rabe 001; Yasmine Sharoda (CICM, 2019)

How to Calculate with Nondeterministic Functions. - Richard S. Bird; Florian Rabe 001 (MPC, 2019)

Making Isabelle Content Accessible in Knowledge Representation Formats. - Michael Kohlhase; Florian Rabe 001; Makarius Wenzel (TYPES, 2019)

Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal. - Jacques Carette; William M. Farmer; Michael Kohlhase; Florian Rabe 001 (CoRR, 2019)

TGView3D System Description: 3-Dimensional Visualization of Theory Graphs. - Richard Marcus; Michael Kohlhase; Florian Rabe 001 (CoRR, 2019)

Rapid Prototyping Formal Systems in MMT: 5 Case Studies. - Dennis Müller 001; Florian Rabe 001 (LFMTP@LICS, 2019)

Logic-Independent Proof Search in Logical Frameworks - (Short Paper). - Michael Kohlhase; Florian Rabe 001; Claudio Sacerdoti Coen; Jan Frederik Schaefer (IJCAR (1), 2020)

Representing Structural Language Features in Formal Meta-languages. - Dennis Müller 001; Florian Rabe 001; Colin Rothgang; Michael Kohlhase (CICM, 2020)

Towards a Heterogeneous Query Language for Mathematical Knowledge. - Katja Bercic; Michael Kohlhase; Florian Rabe 001 (CICM, 2020)

A Survey of Languages for Formalizing Mathematics. - Cezary Kaliszyk; Florian Rabe 001 (CICM, 2020)

TGView3D: A System for 3-Dimensional Visualization of Theory Graphs. - Richard Marcus; Michael Kohlhase; Florian Rabe 001 (CICM, 2020)

Structure-Preserving Diagram Operators. - Navid Roux; Florian Rabe 001 (WADT, 2020)

The Space of Mathematical Software Systems - A Survey of Paradigmatic Systems. - Katja Bercic; Jacques Carette; William M. Farmer; Michael Kohlhase; Dennis Müller 001; Florian Rabe 001; Yasmine Sharoda (CoRR, 2020)

(Deep) FAIR mathematics. - Katja Bercic; Michael Kohlhase; Florian Rabe 001 (it Inf. Technol., 2020)

A Language with Type-Dependent Equality. - Florian Rabe 001 (CICM, 2021)

A New Export of the Mizar Mathematical Library. - Colin Rothgang; Artur Kornilowicz; Florian Rabe 001 (CICM, 2021)

Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style. - Florian Rabe 001; Navid Roux (LFMTP, 2021)

Experiences from Exporting Major Proof Assistant Libraries. - Michael Kohlhase; Florian Rabe 001 (J. Autom. Reason., 2021)

Theorem Proving in Dependently-Typed Higher-Order Logic. - Colin Rothgang; Florian Rabe 001; Christoph Benzmüller (CADE, 2023)

Morphism Equality in Theory Graphs. - Florian Rabe 001; Franziska Weber (CICM, 2023)

Extracting Theory Graphs from Aldor Libraries. - Florian Rabe 001; Stephen M. Watt (CICM, 2023)

Theorem Proving in Dependently-Typed Higher-Order Logic - Extended Preprint. - Colin Rothgang; Florian Rabe 001; Christoph Benzmüller (CoRR, 2023)

Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401). - Andrej Bauer; Katja Bercic; Florian Rabe 001; Nicolas M. Thiéry; Jure Taslak (Dagstuhl Reports, 2023)

A Logical Framework Perspective on Conservativity. - Florian Rabe 001 (CICM, 2024)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)

The Potential of Answer Classes in Large-scale Written Computer-Science Exams - Vol. 2. - Dominic Lohr; Marc Berges; Michael Kohlhase; Florian Rabe 001 (CoRR, 2025)

Formalizing Representation Theorems for a Logical Framework with Rewriting. - Thomas Traversié; Florian Rabe 001 (CoRR, 2025)

Subtyping in DHOL - Extended preprint. - Colin Rothgang; Florian Rabe 001 (CoRR, 2025)

The Dependently Typed Higher-Order Form for the TPTP World. - Daniel Ranalter; Cezary Kaliszyk; Florian Rabe 001; Geoff Sutcliffe (CoRR, 2025)