JEFL: joint embedding of formal proof libraries
From MaRDI portal
Publication:831932
DOI10.1007/978-3-030-86205-3_9OpenAlexW3200624497WikidataQ108482099 ScholiaQ108482099MaRDI QIDQ831932FDOQ831932
Authors: Qingxiang Wang, Cezary Kaliszyk 
Publication date: 24 March 2022
Full work available at URL: https://arxiv.org/abs/2107.10188
Cites Work
- 30 years of research and development around Coq
- The MMT API: a generic MKM system
- The TPTP World -- infrastructure for automated reasoning
- Title not available (Why is that?)
- MPTP 0.2: Design, implementation, and initial experiments
- HOL(y)Hammer: online ATP service for HOL Light
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- HOL Light: An Overview
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Recycling proof patterns in Coq: case studies
- Lemma Mining over HOL Light
- Scalable LCF-style proof translation
- Aligning concepts across proof assistant libraries
- Classification of alignments between concepts of formal mathematical systems
- Sharing HOL4 and HOL Light proof knowledge
- Structured formal development with quotient types in Isabelle/HOL
- Matching concepts across HOL libraries
- Importing HOL Light into Coq
Uses Software
This page was built for publication: JEFL: joint embedding of formal proof libraries
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q831932)
