7 citations · 58 across the 20 of their papers we have counts for
23 papers
Polymorphism Meets DHOL
Rhea Ranalter, Florian Rabe, Cezary Kaliszyk
DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-b…
The Potential of Answer Classes in Large-scale Written Computer-Science Exams -- Vol. 2
Dominic Lohr, Marc Berges, Michael Kohlhase +1
Students' answers to tasks provide a valuable source of information in teaching as they result from applying cognitive processes to a learning content addressed in the task. Due to…
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
Colin Rothgang, Florian Rabe, Christoph Benzmüller
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types…
Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style
Florian Rabe, Navid Roux
Type theories can be formalized using the intrinsically (hard) or the extrinsically (soft) typed style. In large libraries of type theoretical features, often both styles are prese…
A Survey of Languages for Formalizing Mathematics
Cezary Kaliszyk, Florian Rabe
In order to work with mathematical content in computer systems, it is necessary to represent it in formal languages. Ideally, these are supported by tools that verify the correctne…
Making Isabelle Content Accessible in Knowledge Representation Formats
Michael Kohlhase, Florian Rabe, Makarius Wenzel
The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adeq…