Bid to host ITP 2012 at Princeton University

The programming languages group at Princeton University offers to host ITP 2012, the International Conference on Interactive Theorem Proving.

Princeton's distinctive history in logic, computation, and reasoning will provide a stimulating background for a successful conference, and plan to integrate aspects of this heritage into the conference schedule. 2012 is the Centennial of Alan Turing's birth; Turing came to Princeton to do his PhD in the 1930s under Alonzo Church and in consultation with Kurt Gödel.

Venue

We offer to host ITP in the first half of August 2012, on university premises. As a consequence, we envision a comparatively low registration fee, and we can offer accommodation in student dormitories as an alternative to hotel accommodation. The University will not charge a fee for the use of its meeting facilities, and will rent dormitory space and provide catering at reasonable prices. (For catering service such as coffee breaks and meals, we are not restricted to using University food services.) We have provisionally booked lecture theatres and additional facilities at the Friend Center, directly adjacent to the Computer Science department on Princeton's main campus. This is the same location where CAV'08 was held.

Friend Center, seen from Computer Science building

Organizers, program committee

The general co-chairs and local-arrangement co-chairs will be

Lennart Beringer (eberinge@cs.princeton.edu) and
Andrew Appel (appel@cs.princeton.edu) .

We expect that the ITP steering committee will appoint a program chair and program committee who will decide on the exact length and format of the conference; our venue offers significant flexibility on these details. The format of conference proceedings would also be decided by the steering committee and the program chair.

In addition to the scientific program, the schedule will include an excursion, conference dinner, and a further informal social event.

Walkway along computer science building

The Department of Computer Science at Princeton has a history dating back to the early days of computer science, with significant work in digital signal processing, compilers, graphics, and computational complexity theory dating back to the 1960s and 1970s. The current research interests of the hosting group concerns theory and practice of programming languages, ranging from functional languages, compilers, type systems, to program verification and program logics. There has been substantial use of interactive theorem proving at Princeton for over a decade, including the Foundational Proof-Carrying Code project (1999-2005), the Concurrent C Minor project (2005-2010), and the Verified Software Toolchain project (2010-?), using λProlog, Twelf, Coq, and Isabelle/HOL.
Computer Science building

Holding ITP in 2012 in Princeton appears particularly timely, as it would precede the special year on univalent foundations of mathematics at the Institute for Advanced Study, increasing the visibility of interactive theorem proving to the mathematics community.

Local information

The town of Princeton is located halfway between New York and Philadelphia, about 1 hour by public transport from either city. Newark International Airport (EWR) is 45 minutes away with frequent train service directly to the Princeton campus. There are direct flights to EWR from most of the world's major cities. Together with the airports of Philadelphia (PHL) and New York (JFK) it serves virtually all domestic and international destinations. Princeton Station is a stop of the East Coast Corridor train line, with Amtrak train service to many cities on the east coast and beyond.

Several U.S. interactive-theorem-proving research groups are nearby, which will make it easy for students and faculty to attend the conference:

Within 1 hour drive or train ride:: Rutgers University, University of Pennsylvania, Stevens Institute of Technology, New York University
Within 2 hours:: Univ. of Maryland, Lehigh Univ.
Within 3 hours: Yale University, Naval Research Lab
Within 6 hours (or 1 hour flight): Carnegie Mellon Univ., Harvard, MIT, etc.

Princeton is compact and walkable. Dormitories and the Nassau Inn hotel are within 1 km of the conference site. Other hotels are within 3-5 kilometers with free shuttle service to the campus.
There are approximately 40 restaurants within 1 km of the conference site, in a wide variety of price ranges and cuisines.

Google: restaurants near William St & Olden St, Princeton, NJ 08540

The weather in August in Princeton typically is warm, between 27 and 32 Celsius. Conference venue, hotels, and many of the dormitories are air-conditioned. (We believe we can arrange that all of the dormitories booked for this conference will be air-conditioned.)

We'd be looking forward to welcoming the ITP community to our university and are happy to receive questions on further details of our plans.