Florian Rabe - RankMe

120 papers A* 1A 4B 2C 27Journal 39Unranked 40

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Formalizing Representation Theorems for a Logical Framework with Rewriting. CoRR Thomas Traversié, Florian Rabe
2025	A*	`conf`	Formally Verified Cloud-Scale Authorization. ICSE Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Sam Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clément Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas G. Wagner, Michael W. Whalen, Remy Willems, Tongtong Xiang, Tae Joon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan
2025	C	`conf`	Global, Regional, and Local Contexts. CICM Florian Rabe
2025	C	`conf`	Lightweight Realms. CICM Michael Kohlhase, Florian Rabe, Marcel Schütz
2025	J	`jnl`	Subtyping in DHOL - Extended preprint. CoRR Colin Rothgang, Florian Rabe
2025	—	`conf`	Subtyping in Dependently-Typed Higher-Order Logic. FroCoS Colin Rothgang, Florian Rabe
2025	—	`conf`	The Dependently Typed Higher-Order Form for the TPTP World. FroCoS Daniel Ranalter, Cezary Kaliszyk, Florian Rabe, Geoff Sutcliffe
2025	J	`jnl`	The Dependently Typed Higher-Order Form for the TPTP World. CoRR Daniel Ranalter, Cezary Kaliszyk, Florian Rabe, Geoff Sutcliffe
2025	J	`jnl`	The Potential of Answer Classes in Large-scale Written Computer-Science Exams - Vol. 2. CoRR Dominic Lohr, Marc Berges, Michael Kohlhase, Florian Rabe
2024	C	`conf`	A Logical Framework Perspective on Conservativity. CICM Florian Rabe
2024	—	`ed.`	Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2024, Tallinn, Estonia, 8th July 2024. LFMTP@FSCD Florian Rabe, Claudio Sacerdoti Coen
2023	J	`jnl`	Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401). Dagstuhl Reports Andrej Bauer, Katja Bercic, Florian Rabe, Nicolas M. Thiéry, Jure Taslak
2023	C	`conf`	Extracting Theory Graphs from Aldor Libraries. CICM Florian Rabe, Stephen M. Watt
2023	C	`conf`	Morphism Equality in Theory Graphs. CICM Florian Rabe, Franziska Weber
2023	J	`jnl`	Theorem Proving in Dependently-Typed Higher-Order Logic - Extended Preprint. CoRR Colin Rothgang, Florian Rabe, Christoph Benzmüller
2023	A	`conf`	Theorem Proving in Dependently-Typed Higher-Order Logic. CADE Colin Rothgang, Florian Rabe, Christoph Benzmüller
2021	C	`conf`	A Language with Type-Dependent Equality. CICM Florian Rabe
2021	C	`conf`	A New Export of the Mizar Mathematical Library. CICM Colin Rothgang, Artur Kornilowicz, Florian Rabe
2021	J	`jnl`	Experiences from Exporting Major Proof Assistant Libraries. J. Autom. Reason. Michael Kohlhase, Florian Rabe
2021	—	`conf`	Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style. LFMTP Florian Rabe, Navid Roux
2020	J	`jnl`	(Deep) FAIR mathematics. it Inf. Technol. Katja Bercic, Michael Kohlhase, Florian Rabe
2020	C	`conf`	A Survey of Languages for Formalizing Mathematics. CICM Cezary Kaliszyk, Florian Rabe
2020	J	`jnl`	A Survey of Languages for Formalizing Mathematics. CoRR Cezary Kaliszyk, Florian Rabe
2020	J	`jnl`	Experiences from Exporting Major Proof Assistant Libraries. CoRR Michael Kohlhase, Florian Rabe
2020	—	`conf`	Logic-Independent Proof Search in Logical Frameworks - (Short Paper). IJCAR (1) Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer
2020	J	`jnl`	Making Isabelle Content Accessible in Knowledge Representation Formats. CoRR Michael Kohlhase, Florian Rabe, Makarius Wenzel
2020	C	`conf`	Representing Structural Language Features in Formal Meta-languages. CICM Dennis Müller, Florian Rabe, Colin Rothgang, Michael Kohlhase
2020	—	`conf`	Structure-Preserving Diagram Operators. WADT Navid Roux, Florian Rabe
2020	C	`conf`	TGView3D: A System for 3-Dimensional Visualization of Theory Graphs. CICM Richard Marcus, Michael Kohlhase, Florian Rabe
2020	J	`jnl`	The Space of Mathematical Software Systems - A Survey of Paradigmatic Systems. CoRR Katja Bercic, Jacques Carette, William M. Farmer, Michael Kohlhase, Dennis Müller, Florian Rabe, Yasmine Sharoda
2020	C	`conf`	Towards a Heterogeneous Query Language for Mathematical Knowledge. CICM Katja Bercic, Michael Kohlhase, Florian Rabe
2019	J	`jnl`	Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal. CoRR Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe
2019	C	`conf`	Diagram Combinators in MMT. CICM Florian Rabe, Yasmine Sharoda
2019	B	`conf`	How to Calculate with Nondeterministic Functions. MPC Richard S. Bird, Florian Rabe
2019	C	`conf`	Integrating Semantic Mathematical Documents and Dynamic Notebooks. CICM Kai Amann, Michael Kohlhase, Florian Rabe, Tom Wiesing
2019	—	`ed.`	Joint Proceedings of the CME-EI, FMM, CAAT, FVPS, M3SRD, OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2018 co-located with the 11th Conference on Intelligent Computer Mathematics (CICM 2018), Hagenberg, Austria, August 13-17, 2018. CICM Workshops Osman Hasan, Abdou Youssef, Adam Naumowicz, William M. Farmer, Cezary Kaliszyk, Diane Gallois-Wong, Florian Rabe, Gabriel Dos Reis, Grant O. Passmore, James H. Davenport, Markus Pfeiffer, Michael Kohlhase, Serge Autexier, Sofiène Tahar, Thomas Koprucki, Umair Siddique, Walther Neuper, Wolfgang Windsteiger, Wolfgang Schreiner, Wolfram Sperber, Zoltán Kovács
2019	C	`conf`	MMTTeX: Connecting Content and Narration-Oriented Document Formats. CICM Florian Rabe
2019	—	`conf`	Making Isabelle Content Accessible in Knowledge Representation Formats. TYPES Michael Kohlhase, Florian Rabe, Makarius Wenzel
2019	—	`conf`	Rapid Prototyping Formal Systems in MMT: 5 Case Studies. LFMTP@LICS Dennis Müller, Florian Rabe
2019	C	`conf`	Relational Data Across Mathematical Libraries. CICM Andrea Condoluci, Michael Kohlhase, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen, Makarius Wenzel
2019	J	`jnl`	TGView3D System Description: 3-Dimensional Visualization of Theory Graphs. CoRR Richard Marcus, Michael Kohlhase, Florian Rabe
2019	C	`conf`	The Coq Library as a Theory Graph. CICM Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen
2019	C	`conf`	Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation. CICM Katja Bercic, Michael Kohlhase, Florian Rabe
2018	J	`jnl`	A Modular Type Reconstruction Algorithm. ACM Trans. Comput. Log. Florian Rabe
2018	C	`conf`	Automatically Finding Theory Morphisms for Knowledge Management. CICM Dennis Müller, Michael Kohlhase, Florian Rabe
2018	C	`ed.`	Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings CICM Florian Rabe, William M. Farmer, Grant O. Passmore, Abdou Youssef
2018	—	`conf`	Structuring Theories with Implicit Morphisms. WADT Florian Rabe, Dennis Müller
2018	A	`conf`	Theories as Types. IJCAR Dennis Müller, Florian Rabe, Michael Kohlhase
2017	—	`conf`	Alignment-based Translations Across Formal Systems Using Interface Theories. PxTP Dennis Müller, Colin Rothgang, Yufei Liu, Florian Rabe
2017	J	`jnl`	Canonical Selection of Colimits. CoRR Till Mossakowski, Florian Rabe, Mihai Codescu
2017	C	`conf`	Classification of Alignments Between Concepts of Formal Mathematical Systems. CICM Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe
2017	J	`jnl`	How to identify, translate and combine logics? J. Log. Comput. Florian Rabe
2017	C	`ed.`	Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings CICM Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, Olaf Teschke
2017	—	`conf`	Knowledge-Based Interoperability for Mathematical Software Systems. MACIS Michael Kohlhase, Luca De Feo, Dennis Müller, Markus Pfeiffer, Florian Rabe, Nicolas M. Thiéry, Victor Vasilyev, Tom Wiesing
2017	B	`conf`	Making PVS Accessible to Generic Services by Interpretation in a Universal Format. ITP Michael Kohlhase, Dennis Müller, Sam Owre, Florian Rabe
2017	J	`jnl`	Morphism axioms. Theor. Comput. Sci. Florian Rabe
2017	—	`conf`	Virtual Theories - A Uniform Interface to Mathematical Knowledge Bases. MACIS Tom Wiesing, Michael Kohlhase, Florian Rabe
2016	—	`conf`	A Standard for Aligning Mathematical Concepts. FM4M/MathUI/ThEdu/DP/WIP@CIKM Cezary Kaliszyk, Michael Kohlhase, Dennis Müller, Florian Rabe
2016	—	`conf`	Canonical Selection of Colimits. WADT Till Mossakowski, Florian Rabe, Mihai Codescu
2016	C	`conf`	Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach. CICM 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
2016	J	`jnl`	QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge. J. Formaliz. Reason. Michael Kohlhase, Florian Rabe
2016	—	`conf`	TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. PAAR@IJCAR Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe
2016	J	`jnl`	The Future of Logic: Foundation-Independence. Logica Universalis Florian Rabe
2016	J	`jnl`	Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Reports Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe
2015	—	`ed.`	CICM 2015 - Informal Work in Progress Proceedings, Washington, DC, USA, July 13-17, 2015 CICM (Work in Progress) Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge
2015	C	`conf`	Formal Logic Definitions for Interchange Languages. CICM Feryal Fulya Horozal, Florian Rabe
2015	C	`conf`	Generic Literals. CICM Florian Rabe
2015	C	`ed.`	Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings CICM Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge
2015	J	`jnl`	Lax Theory Morphisms. ACM Trans. Comput. Log. Florian Rabe
2014	—	`conf`	A Logic-Independent IDE. UITP Florian Rabe
2014	C	`conf`	Flexary Operators for Formalized Mathematics. CICM Feryal Fulya Horozal, Florian Rabe, Michael Kohlhase
2014	—	`conf`	MMT Objects. CICM Workshops Florian Rabe
2014	C	`conf`	Towards Knowledge Management for HOL Light. CICM Cezary Kaliszyk, Florian Rabe
2013	—	`conf`	A Universal Machine for Biform Theory Graphs. MKM/Calculemus/DML Michael Kohlhase, Felix Mance, Florian Rabe
2013	J	`jnl`	A Universal Machine for Biform Theory Graphs. CoRR Michael Kohlhase, Felix Mance, Florian Rabe
2013	J	`jnl`	A logical framework combining model and proof theory. Math. Struct. Comput. Sci. Florian Rabe
2013	J	`jnl`	A scalable module system. Inf. Comput. Florian Rabe, Michael Kohlhase
2013	—	`ed.`	Joint Proceedings of the MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at CICM, Bath, UK CICM Workshops Christoph Lange, David Aspinall, Jacques Carette, James H. Davenport, Andrea Kohlhase, Michael Kohlhase, Paul Libbrecht, Pedro Quaresma, Florian Rabe, Petr Sojka, Iain Whiteside, Wolfgang Windsteiger
2013	J	`jnl`	Logical relations for a logical framework. ACM Trans. Comput. Log. Florian Rabe, Kristina Sojakova
2013	—	`conf`	The MMT API: A Generic MKM System. MKM/Calculemus/DML Florian Rabe
2013	J	`jnl`	The MMT API: A Generic MKM System. CoRR Florian Rabe
2013	J	`jnl`	The Mizar Mathematical Library in OMDoc: Translation and Applications. J. Autom. Reason. Mihnea Iancu, Michael Kohlhase, Florian Rabe, Josef Urban
2013	—	`conf`	The Scala-REPL + MMT as a lightweight mathematical user interface. CICM Workshops Mihnea Iancu, Felix Mance, Florian Rabe
2012	J	`jnl`	A Query Language for Formal Mathematical Libraries CoRR Florian Rabe
2012	—	`conf`	A Query Language for Formal Mathematical Libraries. AISC/MKM/Calculemus Florian Rabe
2012	—	`conf`	Compiling Logics. WADT Mihai Codescu, Feryal Fulya Horozal, Aivaras Jakubauskas, Till Mossakowski, Florian Rabe
2012	—	`conf`	Extending MKM Formats at the Statement Level. AISC/MKM/Calculemus Feryal Fulya Horozal, Michael Kohlhase, Florian Rabe
2012	—	`conf`	Management of Change in Declarative Languages. AISC/MKM/Calculemus Mihnea Iancu, Florian Rabe
2012	J	`jnl`	Semantics of OpenMath and MathML3. Math. Comput. Sci. Michael Kohlhase, Florian Rabe
2011	J	`jnl`	A Foundational View on Integration Problems CoRR Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen
2011	—	`conf`	A Foundational View on Integration Problems. Calculemus/MKM Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen
2011	J	`jnl`	A Scalable Module System CoRR Florian Rabe, Michael Kohlhase
2011	—	`conf`	Combining Source, Content, Presentation, Narration, and Relational Representation. Calculemus/MKM Feryal Fulya Horozal, Alin Iacob, Constantin Jucovschi, Michael Kohlhase, Florian Rabe
2011	J	`jnl`	Formalising foundations of mathematics. Math. Struct. Comput. Sci. Mihnea Iancu, Florian Rabe
2011	—	`ed.`	Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings Calculemus/MKM James H. Davenport, William M. Farmer, Josef Urban, Florian Rabe
2011	J	`jnl`	Kripke Semantics for Martin-Löf's Extensional Type Theory Log. Methods Comput. Sci. Steven Awodey, Florian Rabe
2011	—	`conf`	Project Abstract: Logic Atlas and Integrator (LATIN). Calculemus/MKM Mihai Codescu, Feryal Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe
2011	J	`jnl`	Representing model theory in a type-theoretical logical framework. Theor. Comput. Sci. Feryal Fulya Horozal, Florian Rabe
2010	—	`conf`	A Proof Theoretic Interpretation of Model Theoretic Hiding. WADT Mihai Codescu, Feryal Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe
2010	J	`jnl`	Publishing Math Lecture Notes as Linked Data CoRR Catalin David, Michael Kohlhase, Christoph Lange, Florian Rabe, Nikita Zhiltsov, Vyacheslav Zholudev
2010	—	`conf`	Publishing Math Lecture Notes as Linked Data. ESWC (2) Catalin David, Michael Kohlhase, Christoph Lange, Florian Rabe, Nikita Zhiltsov, Vyacheslav Zholudev
2010	—	`conf`	Representing Isabelle in LF LFMTP Florian Rabe
2010	—	`conf`	Towards Logical Frameworks in the Heterogeneous Tool Set Hets. WADT Mihai Codescu, Feryal Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe, Kristina Sojakova
2010	J	`jnl`	Towards MKM in the Large: Modular Representation and Scalable Software Architecture CoRR Michael Kohlhase, Florian Rabe, Vyacheslav Zholudev
2010	—	`conf`	Towards MKM in the Large: Modular Representation and Scalable Software Architecture. AISC/MKM/Calculemus Michael Kohlhase, Florian Rabe, Vyacheslav Zholudev
2009	—	`conf`	A practical module system for LF. LFMTP Florian Rabe, Carsten Schürmann
2009	—	`conf`	Integrating Web Services into Active Mathematical Documents. Calculemus/MKM Jana Giceva, Christoph Lange, Florian Rabe
2009	—	`conf`	Kripke Semantics for Martin-Löf's Extensional Type Theory. TLCA Steven Awodey, Florian Rabe
2009	—	`conf`	Representing Model Theory in a Type-Theoretical Logical Framework. LSFA Feryal Fulya Horozal, Florian Rabe
2009	J	`jnl`	Solving the $100 modal logic challenge. J. Appl. Log. Florian Rabe, Petr Pudlák, Geoff Sutcliffe, Weina Shen
2008	—	`conf`	An Exchange Format for Modular Knowledge. LPAR Workshops Florian Rabe, Michael Kohlhase
2008	—	`conf`	Evaluation of Systems for Higher-order Logic (ESHOL). PAAR/ESHOL Christoph Benzmüller, Florian Rabe, Carsten Schürmann, Geoff Sutcliffe
2008	—	`conf`	Flyspeck in a Semantic Wiki. SemWiki Christoph Lange, Sean McLaughlin, Florian Rabe
2008	—	`conf`	Notations for Living Mathematical Documents. AISC/MKM/Calculemus Michael Kohlhase, Christine Müller, Florian Rabe
2008	—	`—`	Representing logics and logic translations. Florian Rabe
2008	—	`ch.`	Repräsentation von Logiken und Logik-Übersetzungen [Representing Logics and Logic Translations]. Ausgezeichnete Informatikdissertationen Florian Rabe
2008	A	`conf`	THF0 - The Core of the TPTP Language for Higher-Order Logic. IJCAR Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe
2008	—	`conf`	Translating a Dependently-Typed Logic to First-Order Logic. WADT Kristina Sojakova, Florian Rabe
2007	J	`jnl`	An Institutional View on Categorical Logic. Int. J. Softw. Informatics Joseph A. Goguen, Till Mossakowski, Valeria de Paiva, Florian Rabe, Lutz Schröder
2006	A	`conf`	First-Order Logic with Dependent Types. IJCAR Florian Rabe