1 citations · 1 across the 2 of their papers we have counts for
3 papers
cs.LO2015★ 1 cited
The Common HOL Platform
Mark Adams
The Common HOL project aims to facilitate porting source code and proofs between members of the HOL family of theorem provers. At the heart of the project is the Common HOL Platfor…
math.MG2015
A formal proof of the Kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer +19
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the…
cs.LO2013
Capturing Hiproofs in HOL Light
Steven Obua, Mark Adams, David Aspinall
Hierarchical proof trees (hiproofs for short) add structure to ordinary proof trees, by allowing portions of trees to be hierarchically nested. The additional structure can be used…