December 4th at 17:30, in ILLC Seminar Room (F1.15)
This talk is about two pieces of my most recent work: ProofCloud and HOLALA: ProofCloud: I will first introduce ProofCloud, a proof retrieval engine for verified higher order proofs. ProofCloud provides a fast proof searching service for mathematicians and computer scientists for the reuse of proofs and proof packages. I will also include a first statistical analysis of higher order proofs and the first complete proof checking results and benchmarks for higher order proofs of the OpenTheory repository. HOLALA: For the sake of reliability, the kernels of Interactive Theorem Provers (ITPs) are kept relatively small in general. On top of the kernel, additional symbols and inference rules are defined. Some dependency analysis of symbols of HOL Light indicates that the depth of dependency could be reduced by introducing few more symbols to the kernel. In the second part of this talk, I will extend the kernel of HOL Light and explain how this reduce the proof size.