These minutes are by Matt Kaufmann, from an attempt to take notes. Apologies for any inaccuracies! Corrections are welcome.
Financing was handled this time by FLoC. Tobias says that in the last few years, no money was handed down from TPHOLs to TPHOLs. Should ITP should incorporate itself in some country, in order to have a permanent home for its funds and to protect the organisers from legal liability?
Julien Schmaltz said that as ITP 2011 co-chair, he would find such arrangements to be helpful, to avoid financial risk etc.
Ernie Cohen asked about the possibility of taking advantage of the FMCAD administrative structure. Warren Hunt replied that he formed a corporation for FMCAD with his own personal funds and has managed the payment of taxes etc.; a fair amount of work, not recommended. Another drawback: affiliation with ACM or IEEE would be more permanent. Warren pointed out that however, a real company adds negotiation power, while the ACM or IEEE might not be much help. So in that sense he encourages consideration of incorporating, even though ownership issues can be complex.
There was a bit of discussion on corporate sponsorship, but not much came of that.
Michael Norrish said that this issue will be discussed by the Steering Committee, by email.
No bids from outside Europe came by the deadline for bids, so we opened up bidding to the world. Does there need to be an effort to get non-Europe bids for ITP 2012, and if so, what should that be?Bids will go out in about 6 months for ITP 2012.
Elsa Gunter asked what happens if North America makes only one bid and that one is thus chosen. Her concern is that Urbana might not get many attendees. Michael Norrish commented that an affiliated ACL2 workshop could draw from North America. Matt Kaufmann agreed, pointing out that that workshop usually gets about 40 people but has had up to about 60.
Warren Hunt mentioned that Springer is more expensive than the ACM Digital Library, and particularly relevant to this discussion, might lose interest in publishing the proceedings if the attendance is too small. Elsa Gunter said [something like] that perhaps 70 to 80 attendees might need to attend for Springer.
Should the page limit for rough diamonds be increased to 6 pages? How can we encourage more such submissions? Were rough diamonds a good idea?Michael Norrish explained that before the introduction of Rough Diamonds, supplementary proceedings were published locally, often including papers that had been rejected for the regular proceedings.
[I think Michael said that although we are discussing this issue, it's really up to the program chairs, who of course might appreciate guidance.]
Warren Hunt liked the idea of increasing to 6 pages. Nobody dissented. [I think there was a comment that proceedings pages are rather small.] Warren also pointed out that attendance at poster sessions depends a lot on where they are.
Printed proceedings?Ernie Cohen said that that when a rumor started to spread that proceedings might not be published for VSTTE, a number of people started talking about pulling their submissions out.
Paul Jackson pointed out that most FLoC 2010 conferences only ordered their 50 free proceedings copies, but Springer makes money from libraries. There was some sense in the meeting that there was some misunderstanding though, with people thinking that proceedings were included in the registration.
J Moore mentioned that promotion cases have discriminated against online proceedings, though that is likely to change eventually. Yves Bertot pointed out that because of this likely change, there shouldn't be any long-term decision committing to printed proceedings; maybe EPTCS [Electronic Proceedings in Theoretical Computer Science, presumably] eventually.
Warren Hunt said that FMCAD uses ACM/IEEE because of Springer cost. He also mentioned that Univ. of Texas purchases many journals. Pete Manolios said that starting in 2010 FMCAD is operating as follows: the FMCAD steering committee owns the copyrights for the proceeding, and gives ACM and IEEE the right to publish the proceedings in their digital libraries. This allows FMCAD to make all the papers available for free in the FMCAD Web page, and to get the proceeding in the major digital libraries. Pete suggested the ITP consider this publication model. Michael Norrish liked the idea of retaining the copyright.
Tutorials? The minutes of the 2008 TPHOLs business meeting suggest tutorials may be of interest. Of course, that may mean fewer accepted papers.Matt Kaufmann pointed out that it was his idea at the TPHOLs 2008 business meeting to consider tutorials, and he included this in the agenda simply because he felt guilty that he hadn't followed through at ITP 2010. Enough said.
Status of merger with ACL2 Workshop?J Moore said that he likes the name "ITP" and that ACL2 users will contribute papers to ITP, just as they do to CAV and FMCAD. He pointed out that the ACL2 community will consider the question of ACL2 workshops online, after ITP ends.
Michael Norrish pointed out that ACL2 workshops can continue. Cesar Munoz said that workshops do have a place. Someone(s) pointed out that there are Coq workshops and Isabelle even though there is also TPHOLs/ITP.
Peter Homeier said that he welcomes ACL2's participation in ITP, and that a publication at a conference is good for tenure and promotion.
Yves Bertot expressed his view that ITP is the best place to publish papers in the area, and for the best people to attend; a workshop is the best place for discussion of specific techniques; and young researchers' profiles depend on publishing in such conferences.
Others?There was other discussion.
Warren Hunt said that to affiliate with IEEE or the ACM, we'd need 5 to 6 reviews per paper. He pointed out that having over 100 attendees at the first conference meeting is a great start, and we don't want to lose such momentum.
Michael Norrish asked if there is a community not represented. Cesar Munoz suggested that applications could be more strongly welcomed. Elsa Gunter observed that application papers are more difficult to get accepted because referees want to know what's new. She asked: What are out criteria? How much in an application paper has to be new with respect to theorem proving? She added that we need an appropriate PC.
J Moore said that he's happy to see application papers accepted, except they often teach him relatively little. So he would like to see application papers conclude with 3 features of the interactive theorem proving environment that the author really liked and 3 features (or non-features) that almost made the author quit.
Ernie Cohen asked how VSTTE and ITP are fundamentally different. He explained that VSTTE is a meeting about the functional correctness of software. Michael Norrish pointed out that our conference is on interactive theorem proving, and perhaps VSTTE doesn't really emphasize the "interactive". Ernie suggested that VCC and Spec# can be considered interactive, and has since noted that almost all ITP 2010 talks (all but two) are of interest to program verification.
Ernie also suggested allowing arbitrary page lengths and talk time to be requested, where the response would presumably be based on the perceived value of the pages and talk.