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 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 (kaufmann@cs.utexas.edu and
konrad.slind@gmail.com) 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.