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


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 to make the talks accessible.

The following individuals have accepted an invitation to present and lead discussions:

We are also pleased that the following individuals will contribute talks (also with discussions):

We solicit contributed presentations, each of which will be alloted 30 to 45 minutes. Each presentation will start with a prepared talk and conclude with a discussion led by the presenter. The talk may include slides and perhaps a demo, and the presenter will bring questions or remarks to spur the discussion. If you are interested, please send email to Matt Kaufmann and Konrad Slind ( and with a short (1-page maximum) abstract, including discussion questions or remarks.

The following list of topic areas is not intended to be exhaustive, but we hope it gives a sense of what is in scope.