Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval - Archive ouverte HAL Access content directly
Conference Papers Year :

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

(1)
1

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.
Fichier principal
Vignette du fichier
aitp_2016_final.pdf (295.82 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01250197 , version 1 (04-01-2016)

Identifiers

  • HAL Id : hal-01250197 , version 1

Cite

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⟩
103 View
121 Download

Share

Gmail Facebook Twitter LinkedIn More