Possibly Colocated with CADE-29
Middlesex University offers to host the 12th edition of ITP in London, possibly jointly with the 29th edition of Conference on Automated Deduction (CADE-29). Notwithstanding its remarkable tradition in logic and formal methods research, the city of London has never hosted ITP or its TPHOLs predecessor. The same was true for ITP's siblings in the mechanized reasoning family — CADE, FroCoS and TABLEAUX — until the spell was broken in 2019 for FroCoS and TABLEAUX. ITP and CADE will hopefully follow suit.
The conference will be organized by Andrei Popescu, who is a Senior Lecturer at Middlesex University and a member of the research groups on Foundations of Computing and Applied Software Engineering. In recent years, these groups have organized (or are in the process of organizing) events dedicated to theorem proving, verification and theoretical computer science. Examples include the 31st British Colloquium of Theoretical Computer Science (BCTCS), the 2nd South of England Regional Programming Language Seminar (S-REPLS), and the 2019 joint edition of FroCoS and TABLEAUX. All these events have been totally or partly supported financially by the university and by external sponsors such as Amazon. We will seek similar support for ITP, and have all reasons to be optimistic. This, together with other factors discussed below (including conference rooms free of charge, reasonably-priced catering, reasonably-priced hotels in the area, and cheap student-dorm accommodation for young researchers) should keep fairly low the conference fees and the overall expenses incurred by each participant. All earnings and spendings by the university in relation to this conference will be entirely transparent. We will aim for a zero balance, but otherwise any surplus will go to the ITP budget.
The organizer's own research is deeply rooted in interactive theorem proving, where he worked on a diversity of sub-topics including (co)inductive datatypes, syntax with bindings, logical foundations, proof-assistant automation and verification of information-flow security. He published seven papers in ITP, and other papers in conferences and journals that accept/encourage interactive theorem proving research. He served in the program committees of ITP (in 2016 and 2018) and related conferences such as CPP (in 2015 and 2019), IJCAR (in 2016) and TABLEAUX (in 2015) and is co-organizing and co-chairing FroCoS 2019 and TABLEAUX 2019. Together with colleagues, he has been developing the verified conference management system CoCon, which was deployed for ITP 2016 and TABLEAUX 2015. One of his main research vehicles is the Isabelle proof assistant.
The organizer offers to co-chair the conference, together with
Damien Pous (CNRS, ENS Lyon, France).
Damien has been working with the Coq proof assistant, where he developed libraries and tactics
about relation algebra, Kleene
algebra, and more recently graph theory and approximation theory.
The program committee would be constituted
in a manner that represents the diversity of interactive theorem proving systems and applications, with ratios
that try to
reflect the research activity around them and (to a lesser extent) their user bases.
The chairs' complementary areas of expertise on proof assistants based on higher-order logic
and dependent type theory, respectively, will help to achieve such a diverse representation.
The chairs will favor a larger program committee, which
will help not only with the diverse representation but also with the high quality of the reviews.
They also believe that prolific ITP authorship is an important criterion (among others) when
selecting program committee members.
The organizer considers high participation by junior researchers to be extremely beneficial
to our community.
To this end, he will strive to encourage junior researcher submissions and
participation through various incentives,
including junior best paper and best presentation awards and travel grants.
The ITP and CADE events have an important and growing synergy, with their focus on
two complementary but also highly interconnected topics: interactive theorem
proving (usually specialized in expressive higher-order logics and type theories)
and automated theorem proving (traditionally focused on first-order logic).
Researchers in the two communities have
always cooperated fruitfully, but lately they seem to have reached a remarkable
technical understanding of the other side's
goals and needs, which has led to impressive cooperative results.
The successful integration of first-order
provers with proof assistants on the one hand, and
the substantial progress in the theory and practice
of fully automated higher-order provers on the other hand, are only two examples.
The inclusion of ITP 2020 as part of IJCAR (along with CADE, FroCoS and TABLEAUX) acknowledges
this synergetic trend. However, the complete merging of
the two conferences — which involves appointing a single program committee and having
ITP and CADE submissions compete against each other — may not
be the optimal scheme, given that the scientific evaluation criteria for interactive
and automatic theorem proving are quite different.
For 2021, we propose colocation without merging (as has happened several times before
A bid for CADE will be placed in due course.
The university is happy to accommodate any dates between 1 July 2021 and 10 September 2021.
The 10 September upper limit is important for ensuring the availability of free conference
rooms and of cheap accommodation on the university premises.
The exact dates will be discussed
with the ITP steering committee.
The affiliated workshops and tutorials will be scheduled such that they do not overlap with
the main conference(s). The organizer is flexible about the exact scheduling scheme. A possibility is to have
all workshops and tutorials during one or two days before the main conference(s). In case of colocation with CADE, the two
conferences could take place in parallel, but with avoiding parallel sessions for the invited
talks and for other talks that
the program committee would identify as being of wider/joint interest. A variation of this scheme
would be to have only partial overlap, with one of the conferences starting one day or half-day
Middlesex University is located in
North-West London (the Hendon area),
at about 40 minutes by underground train from London's center.
It has a
beautiful modern campus,
consisting of several buildings and green spaces centered around a glass-covered
Rickett Quadrangle (the Quad).
Arts and Creative Industries,
Professional and Social Sciences,
and Science and Technology, the last of which
contains the departments of Mathematics and Computer Science.
Recent study conducted in the Middlesex campus reveals London is in effect very sunny
Main campus entrance
Ritterman's living wall (top); Homo sapiens (bottom)
The Quand during the day
The Quand during a night concert
Thanks to the vibrant Art Design department, the campus is constantly featuring (mostly modern) art exhibitions. Moreover, the campus has some picturesque or exotic assets, including a model farmhouse and one of the only three medieval-style "real tennis" courts in UK universities, which can be tried by tennis aficionados. Many of the computer science labs are taught in the Ritterman building, whose design incorporates sustainable technologies such as solar panels, a bio-diverse green roof, and living walls irrigated by rainwater harvesting.
Next to the campus there is the 22-hectares wide
Sunny Hill park, a place for discussing science
(or simply escaping some conference talks) while enjoying nature
hilltop view of the neighborhood.
Hendon council chamber
The university has eight modern lecture theaters in the campus, with capacities between 100 and 350 people. Also usable for university-hosted conferences are the vintage rooms of the Hendon Town Hall — such as the Hendon council chamber, an interior design masterpiece with a capacity of 150 people. All rooms (for the conferences and the affiliated workshops) will be available free of charge.
Like they have done for past events, the university's partners will provide high-quality catering at reasonable prices and observing dietary constraints. Here is an example package, currently on offer for £23.10 / day: (1) three refreshments, each including coffee, tea, still and sparkling water and biscuits, one with additional mini-cakes and one with additional fruits plus (2) a hot or cold fork buffet lunch with a variety of options.
The campus has three cafeterias and a food court.
There are also many restaurants, hummus bars and kebab shops located within 5 minutes from the campus. They cover a
bewildering variety of cuisines, such as Chinese, Indian, Italian, Japanese, Mexican, Polish, Portugiese
Standing out is
a very popular sushi restaurant located right next to the university,
a mind-boggling range of sushi variations (including cooked ones),
covering all tastes and diet requirements.
At a 10-minute walk (near the Hendon Central station), there is
one of the finest (though not fussy or expensive) Indian restaurants the organizer
has ever tried.
Many more restaurants are in the nearby
Golders Green area, which is also home of
Jewish bakeries such as
Quick and convenient transportation to and from cities in the UK and abroad is one of London's specialties.
six international airports.
the Luton airport, conveniently located
at less than one hour by public transportation
from Middlesex University, as well as
some of the world's most linked airports:
Heathrow, Gatwick and Stanstead.
London is also well connected to the rest of the UK by means of fast trains, and features an excellent,
wide-covering underground train system.
The Middlesex campus is at 10 minutes walking distance
from both (1) the
station on the London underground Northern line, directly linked to the
railway hub and
Hendon train station,
directly linked with the Gatwick and Luton airports.
While London hotel prices are high on average, the Hendon area has many good-quality / good-deal hotels located close to the Middlesex campus. Regular prices can incur sharp decreases for early bookings. For example, a May 31st room search on a nearby large Premier Inn hotel (23 minutes walking, 10 minutes by bus), shows a total price of £263 for any choice of 5 nights in July, which is the peak of the touristic season. More expensive choices, even closer to the campus, include The Hide and Hendon Hall; these also offer significant discounts for early bookings. The organizer will seek special deals with some of these hotels (which could further decrease the room prices with up to 20% in addition to the early booking), and offer these deals to the participants through the conference website.
For young researchers and other budget-constrained participants, the university
can offer plenty of
accommodation at a £30 daily rate
the excellently maintained
shared flats located close to the campus.
there is the nearby
Backpackers hostel at a £40 daily rate.
Premier Inn room
Affordable Plat Hall room
The welcome reception will likely be hosted in the Grove atrium, a Middlesex campus landmark located in the Arts and Creative Design building. For the main social event, we will consider one or several of the following possibilities:
- a visit to one or more of London's famous museums, combined with a Thames river trip and with the conference banquet;
- a historical introduction to, and a hands-on-racket lesson in real tennis, again in the Middlesex campus;
- a jazz concert at one of Camden Town's iconic music venues;
- an artistic event on the university's own music, theater and fine art scenes within the Faculty of Arts and Creative Design, which has exceptional artists and designers among its academic staff and also attracts artists from all over the world.
Theater studio in the campus
London is best visited during the summer, when the temperatures are ideal
for long walks in the city and its surroundings or for crossing out the nearby
from one's to-definitely-see-sometime list.
Other reasons for a summer visit to London can be found
Main attractions are of course London's museums, many of which are free during the weekend
and are conveniently
clustered in small areas such as