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:STANDARD
DTSTART:20081102T020000
RDATE:20081102T020000
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20090113T000344Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090113T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090113T103000
DTSTAMP;VALUE=DATE-TIME:20090113T000344Z
LAST-MODIFIED;VALUE=DATE-TIME:20090113T000344Z
UID:http://calagator.org/events/1250456454
DESCRIPTION:PRESENTATION
\;\n
\;\nTitle: OpenTheory: Package Manage
ment for Higher Order Logic Theories
\;\n
\;\nSpeaker: Joe Hurd\,
Galois\, Inc.
\;\n
\;\nAbstract:
\;\n
\;\nInteractive theore
m has grown beyond toy examples in mathematics and program verification\
, as demonstrated by recent successes such as the Gonthier's formal proo
f of the four colour theorem and Leroy's verified compiler from a realis
tic subset of C into PowerPC assembly code. As the construction of large
programs led to the development of software engineering techniques\, th
ere is now a need for theory engineering techniques to support these maj
or verification efforts.
\;\n
\;\nIn this talk I will present the
OpenTheory project\, which has defined a simple 'article' format to repr
esent theories of higher order logic. Theories in article format can be
written by one higher order logic theorem prover\, compressed by a stand
alone tool\, stored and read by a different theorem prover. Articles nat
urally support theory interpretations\, which leads to more efficient de
velopments of standard theories\, and also provides one approach to hand
ling difficult constructs such as monads without extending the underlyin
g logic. Finally\, the grand vision of the OpenTheory article repository
is painted\, with fully automatic installation and dependency resolutio
n.
\;\n
\;\nABOUT THE GALOIS TECH TALKS:
\;\n
\;\nGalois (ht
tp://galois.com) has been holding weekly technical seminars for several
years on topics from functional programming\, formal methods\, compiler
and language design\, to cryptography\, and operating system constructio
n\, with talks by many figures from the programming language and formal
methods communities.
\;\n
\;\nThe talks are open and free. If you'
re planning to attend\, dropping a note to donsATgaloisDOTcom is appreci
ated\, but not required. If you're interested in giving a talk\, we're
always looking for new speakers.
\;\n\n\nTags: galois\n\nImported fr
om: http://calagator.org/events/1250456454
URL:http://www.galois.com/blog/2009/01/08/tech-talk-opentheory-package-ma
nagement-for-higher-order-logic-theories/
SUMMARY:Galois Tech Talk: OpenTheory\, Package Management for Higher Orde
r Logic Theories
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:0
END:VEVENT
END:VCALENDAR