Welcome to ITP 2017 in Brasília!

The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009. The eighth ITP conference, ITP 2017, will be held at the University of Brasília, between 26 and 29 September 2017.

ITP 2017 will be co-located with the 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2017) and the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017).

The proceedings for ITP 2017 conference will be published in the Springer series Lecture Notes in Artificial Intelligence (LNAI).

Itamaraty Palace

Call for Papers

ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include but are not limited to the following:

  • formal aspects of hardware and software;
  • formalizations of mathematics;
  • improvements in theorem prover technology;
  • user interfaces for interactive theorem prover;
  • formalizations of computational models
  • verification of security algorithms
  • use of theorem provers in education
  • industrial applications of interactive theorem provers
  • concise and elegant worked examples of formalizations (proof pearls).

All submissions must be original, unpublished, and not submitted concurrently for publication elsewhere. Furthermore, submissions are expected to be accompanied by verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used. Submissions should be no more than 16 pages in length and are to be submitted in PDF via EasyChair at the following address:


Submissions must conform to the LNCS style in LaTeX. The proceedings are to be published as a volume in the Lecture Notes in Computer Science series and will be available to participants at the conference. Authors of accepted papers are expected to present their paper at the conference and will be required to sign a copyright release forms.

In addition to regular papers, described above, there will be a rough diamond section. Rough diamond submissions are limited to 6 pages and may consist of an extended abstract. They will be refereed and be expected to present innovative and promising ideas, possibly in an early form and without supporting evidence. Accepted diamonds will be published in the main proceedings and will be presented as short talks.

Formatting instructions and the LNCS style files can be obtained at:


After the conference the authors of selected papers will be invited to submit revised papers for a special issue of the Journal of Automated Reasoning.

Itamaraty Palace

Important Dates

  • Submission of title and abstracts: Monday, April 3, 2017
  • Submission of full papers: Monday, April 10, 2017
  • Author notification: Friday, June 2, 2017
  • Camera-ready papers: Friday, June 30, 2017
  • Workshops & Tutorials: September 23-25, 2017
  • Main conference: September 26-29, 2017
  • National Congress

    Invited Speakers

  • Katalin Bimbó (University of Alberta, Canada) (joint with TABLEAUX and FroCoS)

    Title: The perimeter of decidability (with sequent calculi on the inside)

    Abstract: Sequent calculi are preeminently capable of controlling the shape of proofs in a logic. Sometimes this allows decidability to be proved. However, formulating certain intensional logics as sequent calculi creates challenges. I will start with sequent calculi for implicational ticket entailment, and highlight some of the key ideas behind a well-behaved sequent calculus, which was (partly) inspired by structurally free logics. The decidability of implicational ticket entailment was an open problem for about 50 years. I will outline a solution using sequent calculi (from Bimbo & Dunn 2012 and 2013).

    The decidability proof of pure relevant implication (Kripke 1959) can be (and has been) utilized differently (than for implicational ticket entailment). I will focus on adding modalities, lattice connectives and structural rules (both in unrestricted and limited forms). Many of the resulting logics are not among the well-known normal modal logics. I will show that certain ways of adding modalities keep the logic decidable. Moreover, the Curry-Kripke method (possibly, with some additions) still can be used to prove their decidability.

  • Jasmin Blanchette (Inria and LORIA, Nancy, France) (joint with TABLEAUX and FroCoS)

    Title: Foundational (Co)datatypes and (Co)recursion for Isabelle/HOL
    Joint work with Julian Biendarra, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, and Dmitriy Traytel

    Abstract: Systems such as Isabelle adhere to the tradition initiated in the 1970s by the LCF system: All inferences are derived by a small trusted kernel; types and functions are defined rather than axiomatized to guard against inconsistencies. In this talk, I will describe a line of work that started in 2011 towards enriching Isabelle/HOL's language with coalgebraic datatypes (which allow infinite values) and with a more expressive notion of algebraic datatypes. These new (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with Agda, Coq, Lean, and Matita, no additional axioms or logic extensions are necessary.

  • Moa Johansson (Chalmers University of Technology, Sweden)
  • Cezary Kaliszyk (University of Innsbruck, Austria) (joint with TABLEAUX and FroCoS)
  • Leonardo de Moura (RISE, Microsoft Research)
  • Federal Prosecution Office

    Program Committee Chairs

  • Mauricio Ayala-Rincon (U. Brasilia)
  • Cesar Munoz (NASA)
  • Program Committee

  • Maria Alpuente (T. U. Valencia)
  • Vander Alves (U. Brasilia)
  • June Andronick (Data61, CSIRO & New South Wales)
  • Jeremy Avigad (Carnegie Mellon U.)
  • Sylvie Boldo (INRIA LRI)
  • Ana Bove (Chalmers & Gothenburg U.)
  • Adam Chlipala (MIT)
  • Gilles Dowek (INRIA, ENS Cachan)
  • Aaron Dutle (NASA)
  • Amy Felty (U. Ottawa)
  • Marcelo Frias (I. T. Buenos Aires)
  • Ruben Gamboa (U. Wyoming)
  • Herman Geuvers (Radboud U.)
  • Elsa Gunter (U. Illinois U. C.)
  • John Harrison (Intel Corporation)
  • Nao Hirokawa (JAIST)
  • Matt Kaufmann (U. Texas Austin)
  • Mark Lawford (McMaster U.)
  • Andreas Lochbihler (ETH Zurich)
  • Assia Mahboubi (INRIA)
  • Panagiotis Manolios (Northeastern U.)
  • Gopalan Nadathur (U. Minnesota)
  • Keiko Nakata (SAP Potsdam)
  • Adam Naumowicz (U. Bialystok)
  • Tobias Nipkow (T. U. Munich)
  • Scott Owens (U. Kent)
  • Sam Owre (SRI)
  • Lawrence Paulson (U. Cambridge)
  • Leila Ribeiro(U. F. Rio Grande do Sul)
  • Claudio Sacerdoti Coen (U. of Bologna)
  • Augusto Sampaio (U. F. Pernambuco)
  • Monika Seisenberger (Swansea U.)
  • Christian Sternagel (U. Innsbruck)
  • Sofiene Tahar (Concordia U.)
  • Christian Urban (King's College London)
  • Josef Urban (Czech T. U. Prague)
  • Catholic Cathedral


    The conference is organised by the Departments of Computer Science and Mathematics at the University of Brasília and by the Departments of Informatics and Applied Mathematics and Mathematics at the Federal University of Rio Grande do Norte.

    Organising Committee:

  • Cláudia Nalon (CIC/UnB)
  • Daniele Nantes Sobrinho (MAT/UnB)
  • Elaine Pimentel (DMAT/UFRN)
  • João Marcos (DIMAp/UFRN)
  • National Museum


    ITP 2017 is the eighth conference on Interactive Theorem Proving and related topics, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. The inaugural meeting of ITP was held on 11 to 14 July 2010 in Edinburgh, Scotland, as part of the Federated Logic Conference (FLoC, 9 to 21 July 2010). ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009.

    The TPHOLs Conference Series

    TPHOLs 2009 was the twenty-second in a series of international conferences on the applications of higher order logic theorem proving. The first three (two at Cambridge and one at Århus) were informal users’ meetings for the HOL system and were the only ones without published papers. Between 1991 and 1995 (Davis, Leuven, Vancouver, Malta, Utah) the conference entertained an increasingly wide field of interest.

    The evolution resulted in the program committee for the meeting in Turku (1996) deeming that the scope of the conference included all reasoning tools for higher order logics and adopted the name TPHOLs, an acronym for Theorem Proving in Higher Order Logics. (The final letter was considered necessary to break the direct connection between the conference and the HOL system.) This decision was strongly endorsed at the business sessions at Turku and Murray Hill (1997).

    An extensive collection of links to various aspects of previous conferences in the series may be found below.

    Associated Communities

    An inspection of the proceedings of recent conferences show that the conference accommodates the user communities of a number of interactive theorem proving systems. The interested reader is referred to the web sites for the following provers:

    AbellaACL2AgdaBelugaCoqHOLIMPSIsabelleLeanLEGOMatitaMizarNuprlProofPowerPVSTLA+ Proof System


    A longstanding convention is that the annual conference should be held in a continent different to the location of the previous meeting. Another tradition is that the organizers for each meeting handle all aspects of the conference for the whole year in consultation with the previous few organizers. This includes selection of the programme committee, editing the proceedings, fund-raising, program, and local arrangements. Another responsibility of the organizers in year n is to call for bids and conduct a poll for the selection of the venue for the conference in year n + 1.

    Past ITP and TPHOLs Conferences

    2016 7th International Conference on Interactive Theorem Proving, Nancy, France, August 22–27, 2016
    2015 6th International Conference on Interactive Theorem Proving, Nanjing, China, August 24–27, 2015
    2014 5th International Conference on Interactive Theorem Proving, Vienna, Austria, July 14–17, 2014,
    associated with FloC and the Vienna Summer of Logic
    2013 4th International Conference on Interactive Theorem Proving, Rennes, France, July 22–26, 2013
    2012 3rd International Conference on Interactive Theorem Proving, Princeton, NJ, US, August 13–15 2012
    2011 2nd International Conference on Interactive Theorem Proving, Nijmegen, The Netherlands, August 22–25 2011
    2010 1st International Conference on Interactive Theorem Proving, Edinburgh, Scotland, July 11–14, 2010
    2009 The 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August 17–20, 2009
    2008 The 21th International Conference on Theorem Proving in Higher Order Logics, Montreal, Canada, August 18–21, 2008
    2007 The 20th International Conference on Theorem Proving in Higher Order Logics, Kaiserslautern, Germany, September 10–13, 2007
    2006 The 19th International Conference on Theorem Proving in Higher Order Logics merged with FloC, Seattle, August 17–20, 2006
    2005 The 18th International Conference on Theorem Proving in Higher Order Logics, Oxford, UK , 22–25 August 2005
    2004 The 17th International Conference on Theorem Proving in Higher Order Logics, Park City, Utah, USA, 14–17 September 2004
    2003 The 16th International Conference on Theorem Proving in Higher Order Logics, Rome, Italy, 9–12 September 2003
    2002 The 15th International Conference on Theorem Proving in Higher Order Logics, Hampton, Virginia, USA, 20–23 August 2002
    2001 The 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, 3–6 September 2001
    2000 The 13th International Conference on Theorem Proving in Higher Order Logics, Portland, Oregon, USA, 14–18 August 2000
    1999 The 12th International Conference on Theorem Proving in Higher Order Logics, Unversity of Nice-Sophia-Antipolis, Nice, France, 14–17 September 1999
    1998 The 11th International Conference on Theorem Proving in Higher Order Logics, The Australian National University, Canberra, Australia, 28 September – 1 October 1998
    1997 The 10th International Conference on Theorem Proving in Higher Order Logics, Bell Labs, Murray Hill, New Jersey, USA, 19–22 August 1997
    1996 The 9th International Conference on Theorem Proving in Higher Order Logics, Turku Center for Computer Science and Åbo Akademi University, Turku, Finland, 26–30 August 1996
    1995 The 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah, USA, 11–14 September 1995
    1994 The 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, Valletta, Malta, 19–22 September 1994
    1993 The 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver, B.C., Canada, 10–13 August 1993
    1992 The 5th International Workshop on Higher Order Logic Theorem Proving and its Applications, IMEC, Leuven, Belgium, 21–24 September 1992
    1991 The 4th International Workshop on the HOL Theorem Proving System and its Applications, Davis, California, USA, 28–30 August 1991
    1990 The 3rd International HOL Users Meeting, Aarhus University, Denmark, 1–2 October 1990
    1989 The 2nd International HOL Users Meeting, Trinity Hall, Cambridge, 14–15 December 1989
    1988 The 1st International HOL Users Meeting, Sidney Sussex College, Cambridge, 29–30 September 1988
    Itamaraty Palace

    Call for Workshop/Tutorials:

    Following the long tradition of TABLEAUX, FroCoS, and ITP, we invite researchers and practitioners to submit proposals for co-located workshops and in-depth tutorials on topics relating to automated theorem proving and its applications. Workshops/tutorials can target the automated reasoning community in general, focus on a particular theorem proving system, or highlight more specific issues or recent developments.

    Co-located events will take place between 23 and 24/25 September and will be held on the same premises as the main conference. Conference facilities are offered free of charge to the organisers. Workshop/tutorial-only attendees will enjoy a significantly reduced registration fee.

    Detailed organisational matters such as paper submission and review process, or publication of proceedings, are up to the organisers of individual workshops. All accepted workshops/tutorials will be expected to have their program ready by 18 August 2017.

    Proposals for workshops/tutorials should contain at least the following pieces of information:

  • name and contact details of the main organiser(s)
  • (if applicable:) names of additional organisers
  • title and organisational style of event (tutorial, public workshop, project workshop, etc.)
  • preferred length of workshop (between half day and two days)
  • estimated number of attendees
  • short (up to one page) description of topic
  • (if applicable:) pointers to previous editions of the workshop, or to similar events
  • Proposals are invited to be submitted by email to nalon@unb.br, no later than 9 December 2016. Selected events will be notified by 23 December 2016. The workshop/tutorial selection committee consists of the TABLEAUX, FroCoS, and ITP program chairs and the conference organisers.

    JK Bridge

    Co-located Events


  • 12th Logical and Semantic Frameworks with Applications (LSFA 2017)
    Sandra Alves, Renata Wassermann, Flávio L. C. de Moura
    23 and 24 September 2017
  • Proof eXchange for Theorem Proving (PxTP)
    Catherine Dubois, Bruno Woltzenlogel Paleo
    23 and 24 September 2017
  • EPS - Encyclopedia of Proof Systems
    Giselle Reis, Bruno Woltzenlogel Paleo
    24 and 25 September 2017
  • DaLí – Dynamic Logic: new trends and applications
    Mário Benevides, Alexandre Madeira
    24 September 2017
  • Tutorials:

  • Proof compressions and the conjecture NP = PSPACE
    Lew Gordeev, Edward Hermann Haeusler
    23 September 2017
  • General methods in proof theory for modal and substructural logics
    Björn Lellmann, Revantha Ramanayake
    24 September 2017
  • From proof systems to complexity bounds
    Anupam Das
    25 September 2017
  • PVS for Computer Scientists
    César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato
    25 September 2017
  • Brasilia at night (Copyright by Nasa)

    Call for Posters

    TABLEAUX/FroCoS/ITP 2017 will have a poster session, which is intended for descriptions of works in progress, student projects and relevant research being published elsewhere. Submissions should be in English, in the form of at most one page abstract, ENTCS format containing title and authors name with affiliation. The files should be sent directly to Elaine Pimentel (elaine at mat.ufrn.br).

    The deadline for posters submission is June 15, 2017. The notification will be sent to authors June 30th.

    Proceedings of this session will not be published. Formatting instructions for posters will be made available soon.

    For more information please contact the local organizers:

  • Elaine Pimentel (elaine at mat.ufrn.br)
  • Daniele Nantes (dnantes at mat.unb.br)
  • Brasilia at night

    Grants and Financial Support

    Association for Symbolic Logic

    TABLEAUX 2017, FroCoS 2017, and ITP 2017 are officially supported by the Association for Symbolic Logic. Students who are ASL members can apply for (limited) ASL travel funds. Applications should be sent three months prior to the start of the events. For full instructions, visit the ASL Travel Awards page.


    ACM-W provides support for women undergraduate and graduate students in Computer Science and related programs to attend research conferences. It is not required to have a paper to present at the conferences. Applications for conferences which are held in September should be sent until 15 June. Please note that this deadline is strict. For full instructions, please visit their scholarship page.

    Chancellery Building - UnB

    Designed by Mangasanta Arte e Design. Maintained by Cláudia Nalon. Last Updated: