Workshop on Trusted Extensions of Interactive Theorem Provers
Cambridge, UK
Hicks Room, Floor 1, University Centre (on this map, which also shows nearby hotels)
August 11-12, 2010

Organizers: Matt Kaufmann and Konrad Slind
Local Arrangements: Mike Gordon

A fundamental strength of interactive theorem provers (ITPs) is the high degree of trust one can place in formalizations carried out in them. ITPs are usually also extensible, both at the logic level and at the implementation level. There is consequently a substantial body of existing and ongoing research into the extension of ITPs while preserving trust. We hope that this workshop will raise awareness of that work within the ITP community, while stimulating new research. An outcome could be a web page cataloguing approaches to making trusted extensions of ITPs.

We want this to be a workshop that attendees feel is personally useful. Thus, it is expected to have a rather practical orientation, with considerable time reserved for discussion. We expect that talks will report on existing work that may not be well-known to the general ITP community, as well as current or even proposed research. The focus will be on the user level, with sufficient demos and background expected to make the talks accessible. Talks will generally include discussions lead by the speakers.

SUMMARY

Interesting discussion was generated during and after the workshop. See also a taxonomy of trusted extensions for one way of looking at the workshop topic.

PROGRAM

Wednesday, August 11: Day 1
8:30 Coffee and Tea
9:00 Matt Kaufmann
Konrad Slind
Welcome:
[Announcements]
9:15 J Strother Moore Support for ``Trusted'' Extension in ACL2
[Abstract] [Slides]
10:00 Matt Kaufmann Trusted Extension of ACL2 System Code: Towards an Open Architecture
[Abstract] [Slides] (And extra material: [Demo input] [Demo log])
10:30 Coffee and Tea
11:00 Burkhart Wolff Plugins for the Isabelle Platform: A Perspective for Logically Safe, Extensible, Powerful and Interactive Formal Method Tools
[Abstract] [Slides]
11:45 Tjark Weber Integrating SAT, QBF and SMT Solvers with Interactive Theorem Provers
[Abstract] [Slides]
12:15 Lunch
14:00 David S. Hardin User and Evaluator Expectations for Trusted Extensions
[Abstract] [Slides]
14:45 Ian O'Neill Degrees of trustworthiness: observations arising from the SPARK proof tools and their use
[Abstract] [Slides (PDF)] [Slides (Powerpoint)]
15:15 Coffee and Tea
15:45 Natarajan Shankar The Kernel of Truth
[Abstract] [Slides]
16:30 Rob Arthan (speaker)
Joe Hurd
Portable Higher Order Logic Proofs
[Abstract] [Slides]
17:00 End of presentations for Day 1
17:30 - 19:30 Reception with drinks and nibbles (still in the Hicks room)
Thursday, August 12: Day 2
8:30 Coffee and Tea
9:00 Matt Kaufmann
Konrad Slind
Welcome; Announcements; Summary of Day 1
9:15 Laurent Théry Trusted Extensions in Coq
[Abstract] [Slides] [Slides (without animation)]
10:00 J Strother Moore Milawa: A Self-Verifying Theorem Prover
[Abstract] [Slides]
10:30 Coffee and Tea
11:00 Konrad Slind The HOL-4 Trust Story
[Abstract] [Slides]
11:45 Magnus O. Myreen Trustworthy decompilation: extracting models of machine code inside an ITP
[Abstract] [Slides]
12:15 Lunch
14:00 Larry Paulson The potential of MetiTarski for interactive theorem proving
[Abstract] [Slides]
14:30 Grant Olney Passmore (speaker)
Paul B. Jackson
F. Kirchner
Thoughts on Trusting RAHD Computations
[Abstract] [Slides]
15:00 Coffee and Tea
15:30 ALL Discussion and Summary (see notes from final discussion)
A taxonomy of trusted extensions?
17:00 End of Day 2

LIST OF PARTICIPANTS (alphabetical)

Rob Arthan
Anthony Fox
Georges Gonthier
Mike Gordon
David S. Hardin
Roger Bishop Jones
Matt Kaufmann
Magnus O. Myreen
J Strother Moore
Ian O'Neill
Grant Passmore
Larry Paulson
Natarajan Shankar
Konrad Slind
Daryl Stewart
Laurent Thery
Thomas Tuerk
Tjark Weber
Burkhart Wolff
Early announcement