BEGIN:VCALENDAR
PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN
CALSCALE:GREGORIAN
X-WR-CALNAME:Calagator
METHOD:PUBLISH
VERSION:2.0
BEGIN:VTIMEZONE
TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles
BEGIN:DAYLIGHT
DTSTART:20110313T020000
RDATE:20110313T020000
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20110406T230025Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110412T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110412T103000
DTSTAMP;VALUE=DATE-TIME:20110406T230025Z
LAST-MODIFIED;VALUE=DATE-TIME:20110406T230025Z
UID:http://calagator.org/events/1250460443
DESCRIPTION:Presented by Joe Hurd.
\;\n
\;\nInteractive theorem pro
ving is tackling ever larger formalization and verification projects\, a
nd 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 implemen
tations. The OpenTheory project has developed standards for packaging th
eories of the higher order logic implemented by the HOL family of theore
m provers. What is currently missing is a standard theory library that c
an 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 o
f the HOL family of theorem provers\, and describe the process of instru
menting the HOL Light theorem prover to extract a standardized version o
f its core theory development. We profile the axioms and theorems of our
standard theory library and investigate the performance cost of separat
ing the standard theory library into coherent hierarchical theory packag
es.
\;\n\n\nTags: galois\, tech talk\, formal methods\, opentheory\n\
nImported from: http://calagator.org/events/1250460443
URL:http://corp.galois.com/blog/2011/4/6/tech-talk-the-opentheory-standar
d-theory-library.html
SUMMARY:Galois Tech Talk: The OpenTheory Standard Theory Library
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
END:VCALENDAR