Skip to Main content Skip to Navigation
Conference papers

Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval

Shuai Wang 1, *
* Corresponding author
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : Higher Order Logic has been used in formal mathematics, software verification and hardware verification over the past decades. Recent developments of interactive theorem made sharing proofs between some theorem provers possible. This paper first gives an introduction and an overview of related recent advances, followed by the proof checking benchmarks of a proof sharing repository, namely OpenTheory (after proof transformation by the upgraded Holide). Finally, we introduce ProofCloud, the first proof retrieval engine for higher order proofs.
Document type :
Conference papers
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-01250197
Contributor : Shuai Wang <>
Submitted on : Monday, January 4, 2016 - 2:21:28 PM
Last modification on : Tuesday, July 7, 2020 - 11:52:40 AM

File

aitp_2016_final.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01250197, version 1

Collections

Citation

Shuai Wang. Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval. AITP 2016 - Conference on Artificial Intelligence and Theorem Proving, Apr 2016, Obergurgl, Austria. ⟨hal-01250197⟩

Share

Metrics

Record views

229

Files downloads

283