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.
| 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 | |
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 WolffEarly announcement