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 within FLoC). 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 earlier.

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). The campus accommodates three faculties: Arts and Creative Industries, Professional and Social Sciences, and Science and Technology, the last of which contains the departments of Mathematics and Computer Science.

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 and a beautiful hilltop view of the neighborhood.

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 and Turkish. Standing out is a very popular sushi restaurant located right next to the university, offering 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 some well-known Jewish bakeries such as Carmelli.

Quick and convenient transportation to and from cities in the UK and abroad is one of London's specialties. There are six international airports. These include 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 Hendon Central station on the London underground Northern line, directly linked to the King's Cross railway hub and (2) the 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 in the excellently maintained Plat Hall shared flats located close to the campus. In addition, there is the nearby Backpackers hostel at a £40 daily rate.

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.

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 Stonehenge from one's to-definitely-see-sometime list. Other reasons for a summer visit to London can be found here and here. 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 South Kensington.