The goal of the OpenTheory project is to allow specifications and proofs to be shared between different theorem prover implementations of higher order logic, including HOL Light, HOL4 and ProofPower/HOL. It is hoped that OpenTheory packages are adopted by the higher order logic theorem proving community as a common format to build a standard library of formalized mathematics and verified software.

Get started with OpenTheory by downloading the opentheory tool.

## Milestones

**2011:**Launch of the Gilith OpenTheory Repo to support community development of theory packages.**2010:**First publication of a standard for theory files describing theory packages.**2009:**First release of the open source opentheory tool to process theory packages.**2007:**First publication of a standard for article files containing proofs of theorems.**2004:**The project was initiated by Joe Leslie-Hurd (HOL4) and Rob Arthan (ProofPower).

## Resources

- A higher order logic theory package
*Γ*⊲*Δ*consists of a proof that the theorems in*Δ*logically derive from the assumptions in*Γ*(plus some package meta-data). See the example package theory for more details. - A list of frequently asked questions about OpenTheory.
- There is a mailing list to discuss OpenTheory, where you can get help using or creating theory packages.

## Theorem Prover Interfaces

Here are the current theorem prover implementation interfaces that can read (R) and write (W) theories in OpenTheory format:

Theorem Prover | R/W | Maintainer |
---|---|---|

HOL Light | RW | Joe Leslie-Hurd and Ramana Kumar |

HOL4 | RW | Ramana Kumar |

Isabelle | R | Brian Huffman |

## Publications

- CANONICAL CITATION: Joe Hurd. The OpenTheory standard theory library. In Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors,
*Third International Symposium on NASA Formal Methods (NFM 2011)*, volume 6617 of*Lecture Notes in Computer Science*, pages 177–191. Springer, April 2011. [paper] [bibtex] [talk] - Joe Leslie-Hurd. Maintaining verified software. In Chung-chieh Shan, editor,
*Haskell '13: Proceedings of the 2013 ACM SIGPLAN symposium on Haskell*, pages 71–80. ACM, September 2013. [paper] [bibtex] [talk] - Ramana Kumar.
Challenges in using OpenTheory to transport Harrison's HOL model from HOL Light to HOL4.
In Blanchette and Urban, editors,
*Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013)*, volume 14 of EPiC Series, pages 110–116. EasyChair, June 2013. [paper] [bibtex] - Ramana Kumar and Joe Hurd. Standalone tactics using OpenTheory. In Lennart Beringer and Amy Felty, editors,
*Third International Conference on Interactive Theorem Proving (ITP 2012)*, volume 7406 of Lecture Notes in Computer Science, pages 405–411. Springer, August 2012. [paper] [bibtex] - Joe Hurd. Composable packages for higher order logic theories. In M. Aderhold, S. Autexier, and H. Mantel, editors,
*Proceedings of the 6th International Verification Workshop (VERIFY 2010)*, July 2010. [paper] [bibtex] [talk] - Joe Hurd. OpenTheory: Package management for higher order logic theories. In Gabriel Dos Reis and Laurent Théry, editors,
*PLMMS '09: Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems*, pages 31–37, Munich, Germany, August 2009. ACM. [paper] [bibtex] [talk]