research
∙
05/24/2023
Theorem Proving in Dependently-Typed Higher-Order Logic – Extended Preprint
Higher-order logic HOL offers a very simple syntax and semantics for rep...
share
research
∙
07/16/2021
Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style
Type theories can be formalized using the intrinsically (hard) or the ex...
research
∙
05/26/2020
A Survey of Languages for Formalizing Mathematics
In order to work with mathematical content in computer systems, it is ne...
research
∙
05/05/2020
Making Isabelle Content Accessible in Knowledge Representation Formats
The libraries of proof assistants like Isabelle, Coq, HOL are notoriousl...
research
∙
05/05/2020
Experiences from Exporting Major Proof Assistant Libraries
The interoperability of proof assistants and the integration of their li...
research
∙
02/12/2020
The Space of Mathematical Software Systems – A Survey of Paradigmatic Systems
Mathematical software systems are becoming more and more important in pu...
research
∙
10/24/2019
Rapid Prototyping Formal Systems in MMT: 5 Case Studies
Logical frameworks are meta-formalisms in which the syntax and semantics...
research
∙
05/17/2019
TGView3D System Description: 3-Dimensional Visualization of Theory Graphs
We describe TGView3D, an interactive 3D graph viewer optimized for explo...
research
∙
04/23/2019
Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal
Over the last decades, a class of important mathematical results have re...
research
∙
12/05/2017
Alignment-based Translations Across Formal Systems Using Interface Theories
Translating expressions between different logics and theorem provers is ...
research
∙
04/20/2010