Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk: OpenTheory, Package Management for Higher Order Logic Theories</h1> <div class='date'><time class="dtstart dt-start" title="2009-01-13T10:30:00" datetime="2009-01-13T10:30:00">Tuesday, January 13, 2009 from 10:30</time>–<time class="dtend dt-end" title="2009-01-13T11:30:00" datetime="2009-01-13T11:30:00">11:30am</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202390439'><span class='fn org p-name'>Galois, Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 SW 6th Ave. Suite 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>PRESENTATION</p> <p>Title: OpenTheory: Package Management for Higher Order Logic Theories</p> <p>Speaker: Joe Hurd, Galois, Inc.</p> <p>Abstract:</p> <p>Interactive theorem has grown beyond toy examples in mathematics and program verification, as demonstrated by recent successes such as the Gonthier's formal proof of the four colour theorem and Leroy's verified compiler from a realistic subset of C into PowerPC assembly code. As the construction of large programs led to the development of software engineering techniques, there is now a need for theory engineering techniques to support these major verification efforts.</p> <p>In this talk I will present the OpenTheory project, which has defined a simple 'article' format to represent theories of higher order logic. Theories in article format can be written by one higher order logic theorem prover, compressed by a standalone tool, stored and read by a different theorem prover. Articles naturally support theory interpretations, which leads to more efficient developments of standard theories, and also provides one approach to handling difficult constructs such as monads without extending the underlying logic. Finally, the grand vision of the OpenTheory article repository is painted, with fully automatic installation and dependency resolution.</p> <p>ABOUT THE GALOIS TECH TALKS:</p> <p>Galois (<a href="http://galois.com">http://galois.com</a>) 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 construction, with talks by many figures from the programming language and formal methods communities.</p> <p>The talks are open and free. If you're planning to attend, dropping a note to donsATgaloisDOTcom is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://www.galois.com/blog/2009/01/08/tech-talk-opentheory-package-management-for-higher-order-logic-theories/">Website</a></li> </ul> </div>