The CoCon Conference System

Synopsis

Welcome to the CoCon homepage. CoCon is a conference management system developed at the Technical University Munich and at the Middlesex University, London, as part of the RS³ program. It can be used for organizing the process of submitting, discussing and reviewing papers for conferences. It behaves similarly to EasyChair, a popular such system created by Andrei Voronkov. So far, CoCon has been used for the Tableaux 2015 and ITP 2016 conferences.

What makes CoCon special compared to other conference systems is that it is built around a verified core that is guaranteed not to leak. Leakage of course refers to undesired information flow only. In general, a conference system is all about facilitating information flow: authors upload papers for committee members to read and discuss, committee members upload reviews and notifications for authors, etc. However, some information should remain partially or totally secret from some parties. For example, the committee members would surely sleep better if the following type of behavior (exhibited by an older version of HotCRP) did not occur:

We do not mean to suggest that the current HotCRP or EasyChair versions leak confidential information ‒ we certainly hope this is not the case. For CoCon though, we provide assurance.

• How do we know that CoCon does not leak? Because we checked this mechanically in the Isabelle theorem prover. For each type of document (paper, review, discussion, decision), we proved that total or partial information about it may be revealed only under well-defined circumstances, for example:
  • A group of users learn nothing about a paper beyond the last submitted version before the reviewing phase unless one of them is an author of that paper
  • A group of users learn nothing about the content of a review beyond the last submitted version before the discussion phase and the later versions unless one of them is that review's author
  • The authors learn nothing about the discussion of their paper
• How can we be sure that what we proved is faithful to the actual implementation of CoCon? Honestly, one can never be completely sure. However, we designed the system in a way that offers us a lot of confidence that this is the case:
  • We formalize and verify CoCon's kernel in Isabelle
  • The formalization is automatically translated in a functional programming language
  • The translated program is wrapped in a web application that invokes the kernel through a controlled interface

More details can be found in this paper. The formal verification scripts, runnable in Isabelle, can be found here. (We always aim to keep the scrips up to date with the latest Isabelle release ‒ please email Andrei Popescu at uuomulyahoo.com if you encounter any problem with running the scripts.)

Brief Description of the System

CoCon has a superuser, which we call voronkov as a tribute to the EasyChair inspiration. The voronkov is the first user of the system, and his role is to approve new-conference requests. A conference goes through several successive phases.

• No-Phase Any user can apply for a new conference, with the effect of registering it in the system with "No-Phase". After approval from the voronkov, the conference moves to the setup phase, with the applicant becoming a conference chair.
• Setup Any conference chair can add new chairs and new PC members (with a chair also being a PC member). From here on, moving the conference to successor phases can be done by the chairs.
• Submission A user can list the conferences awaiting submissions (i.e., being in submission phase). He can submit a paper, upload new versions, or indicate other users as coauthors thereby granting them reading and editing rights.
• Bidding Authors are no longer allowed to upload or register new papers and PC members are allowed to view the submitted papers. PC members can place bids, indicating for each paper one of the following preferences: "want to review", "would review", "no preference", "would not review", and "conflict". If the preference is "conflict", the PC member cannot be assigned that paper, and will not see its discussion. "Conflict" is assigned automatically to papers authored by a PC member.
• Reviewing Chairs can assign papers to PC members for reviewing either manually or by invoking an external program to establish fair assignment based on some parameters: preferences, number of papers per PC member, and number of reviewers per paper.
• Discussion All PC members having no conflict with a paper can see its reviews and can add comments. Also, chairs can edit the decision.
• Notification The authors can read the reviews and the accept/reject decision, which no one can edit any longer. The authors of accepted papers can upload the camera-ready versions.
• Closed Suitable information about the various documents can still be accessed, but no more posts, uploads or edits are allowed.