The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Hi all,

I am writing a survey paper on proof engineering, and one of the topics is about design principles and frameworks (which often go hand-in-hand).

I'm already aware of a lot of work in this area (planning for changes, writing good automation that is resilient to changes, deep specifications, and principles and frameworks that address problems within certain domains like mechanized metatheory). However, I'm curious if anyone has any useful pointers, especially for folk knowledge -- the kind of thing I might not find looking through old papers, but that everyone who writes proofs about real systems knows and applies in practice.

Of course, if you have papers you'd like to point me to, that's also welcome, since it helps to know if I've missed anything obvious. This doesn't have to be specific to Coq; please feel free to send me something related to other proof assistants like Isabelle. It is particularly interesting to see what exists within one proof assistant but not within another, and whether that is fundamental or simple due to a lack of tooling.

Thanks for all of your help,

Talia Ringer

University of Washington
http://tlringer.github.io/