Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
title: The OpenTheory Standard Theory Library
speaker: Joe Hurd
time: Tuesday, 12 April 2011, 10:30am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
Interactive theorem proving is tackling ever larger formalization and verification projects, and there is a critical need for theory engineering techniques to support these efforts. One such technique is cross-prover package management, which has the potential to simplify the development of logical theories and effectively share theories between different theorem prover implementations. The OpenTheory project has developed standards for packaging theories of the higher order logic implemented by the HOL family of theorem provers. What is currently missing is a standard theory library that can serve as a published contract of interoperability and contain proofs of basic properties that would otherwise appear in many theory packages. This talk will present a standard theory library for higher order logic represented as an OpenTheory package. We identify the core theory set of the HOL family of theorem provers, and describe the process of instrumenting the HOL Light theorem prover to extract a standardized version of its core theory development. We profile the axioms and theorems of our standard theory library and investigate the performance cost of separating the standard theory library into coherent hierarchical theory packages.
bio:
Joe Hurd is a Formal Methods Engineer at Galois, Inc. He completed a Ph.D. at the University of Cambridge on the formal verification of probabilistic programs, and his work since has included: developing a package management system for higher order logic theories; applying automatic proof techniques for first order logic; and creating the world’s first formally verified chess endgame database.