Aligning concepts across proof assistant libraries
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 2043543 (Why is no real title available?)
- scientific article; zbMATH DE number 7015112 (Why is no real title available?)
- 30 years of research and development around Coq
- A Brief Overview of HOL4
- A learning-based fact selector for Isabelle/HOL
- Advanced modern algebra
- Automata, languages and programming. 25th international colloquium, ICALP '98. Aalborg, Denmark, July 13--17, 1998. Proceedings
- Automated Reasoning with Analytic Tableaux and Related Methods
- Category Theory
- Classification of alignments between concepts of formal mathematical systems
- Cooperative Repositories for Formal Proofs
- Data refinement in Isabelle/HOL
- Developing corpus-based translation methods between informal and formal mathematics: project description
- Four decades of \textsc{Mizar}. Foreword
- HOL Light: An Overview
- HOL(y)Hammer: online ATP service for HOL Light
- Hammer for Coq: automation for dependent type theory
- Homotopy type theory. Univalent foundations of mathematics
- Importing HOL Light into Coq
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Learning-assisted theorem proving with millions of lemmas
- MPTP 0.2: Design, implementation, and initial experiments
- Markov chains and dynamical systems: the open system point of view
- Matching concepts across HOL libraries
- Matita Tutorial
- Mizar: state-of-the-art and beyond
- Proceedings Fourth Workshop on Proof eXchange for Theorem Proving
- Recycling proof patterns in Coq: case studies
- Scalable LCF-style proof translation
- Sharing HOL4 and HOL Light proof knowledge
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Stability and convergence in strongly monotone dynamical systems.
- Structured formal development in Isabelle
- Term indexing
- The HOL Light theory of Euclidean space
- The Isabelle Framework
- The Lean theorem prover (system description)
- The MMT API: a generic MKM system
- The TPTP typed first-order form with arithmetic
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- Theorem proving modulo
- Towards Formal Proof Script Refactoring
- What's in a theorem name?
- \textsc{Polar}: a framework for proof refactoring
Cited in
(10)- JEFL: joint embedding of formal proof libraries
- Combining higher-order logic with set theory formalizations
- Matching concepts across HOL libraries
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Recycling proof patterns in Coq: case studies
- Experiences from exporting major proof assistant libraries
- Toward sharing libraries of mathematics between theorem provers
- Learning Proof Transformations and Its Applications in Interactive Theorem Proving
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
Describes a project that uses
Uses Software
This page was built for publication: Aligning concepts across proof assistant libraries
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1640642)
