ITP 2012

ITP 2012 is the third conference on Interactive Theorem Proving and related issues, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics.

CONFERENCE VENUE. The conference and the workshops will be held in Lewis Library on the corner of Washington Road and Ivy lane, here. A MAP highlighting most locations relevant for the conference is here.

Combined ON-SITE REGISTRATION and DORM-CHECK-IN will be available at Scully Hall on Saturday (3pm - 7pm), at Lewis Library during workshop/conference times Sunday - Wednesday, and at Prospect House on Sunday (6pm-8pm). See also the ACCOMMODATION page.

REGISTRATION is now open, including the option to book accommodation in Scully Hall.

The TECHNICAL PROGRAM is now available.

A ROUGH SCHEDULE and information on TRAVEL and ACCOMMODATION are now available.

The list of ACCEPTED PAPERS is now available.

ITP 2013 We're delighted to announce that next year's conference will be held in Rennes, France, organized by the CELTIQUE and ProVal teams of INRIA. Please follow the link to the organizer's web page above!

TUTORIAL. Thank you to Andrew Gacek (Rockwell Collins), who will present a tutorial on Abella.

INVITED SPEAKERS. We're happy to announce that that Gilles Barthe (IMDEA), Lawrence C. Paulson (Cambridge), and Andre Platzer (CMU) all accepted our invitation to present invited talks.

ANNOUNCEMENT OF WORKSHOPS The conference will be preceded by workshops on Isabelle (organized by Tobias Nipkow, Larry Paulson, and Makarius Wenzel) and Coq (organized by Adam Chlipala).

CALL FOR PAPERS. Please follow the link at the top of this page, and take note of the deadlines to the right. As outlined in the CFP, submissions are expected to be complemented by the source files of an implementation. The deadline has now passed.

CALL FOR WORKSHOPS. Please follow the link at the top of this page. Proposals can be submitted until December 5th, 2011. The deadline has now passed.