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 are published in the Springer series Lecture Notes in Computer Science (LNCS), volume 10499and will be freely accessible, as a courtesy of Springer, for registered attendees during the event in the following link:

http://link.springer.com/book/10.1007/978-3-319-66107-0.

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:

http://easychair.org/conferences/?conf=itp2017.

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:

http://www.springer.com/br/computer-science/lncs/conference-proceedings-guidelines.

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) (TABLEAUX/FroCoS/ITP)

    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 (Vrije Universiteit Amsterdam, The Netherlands) (TABLEAUX/FroCoS/ITP)

    Title: Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
    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: We describe a line of work that started in 2011 towards enriching Isabelle/HOL's language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.

  • Moa Johansson (Chalmers University of Technology, Sweden)

    Title: Automated Theory Exploration for Interactive Theorem Proving: An introduction to the Hipster system

    Abstract: Theory exploration is a technique for automatically discovering new interesting lemmas in a mathematical theory development using testing. In this talk I will present the theory exploration system Hipster, which can be used to automatically discover and prove lemmas about a given set of datatypes and functions in Isabelle/HOL.

    This work was originally motivated by attempts to provide a higher level of automation for proofs by induction. Automating inductive proofs is tricky, not least because they often need auxiliary lemmas which themselves need to be proved by induction. We found that many such basic lemmas can be discovered automatically by theory exploration, and importantly, quickly enough for use in conjunction with an interactive theorem prover without boring the user.

    Hipster consists of two main components: the exploration component (called QuickSpec) is implemented in Haskell and efficiently generates candidate conjectures using random testing and heuristics. The conjectures are then passed on to the prover component which is implemented in Isabelle. Hipster can be configured to use various Isabelle tactics, including combining it with Sledgehammer. Hipster discards any conjectures that are trivial to prove and outputs snippets of proof scripts for each interesting lemma it discovers. The user can then easily include these lemmas and their proofs into the Isabelle theory file by a mouse-click.

    The Hipster project is ongoing and open source, with code available from GitHub: http://github.com/moajohansson/IsaHipster. We happily invite those interested in Hipster to try it out and welcome contributions to further development.

  • Cezary Kaliszyk (University of Innsbruck, Austria) (TABLEAUX/FroCoS/ITP)

    Title: Automating Formalization by Statistical and Semantic Parsing of Mathematics

    Abstract: We discuss the progress in our project which aims to automate formalization by combining natural language processing with deep semantic understanding of mathematical expressions. We introduce the overall motivation and ideas behind this project, and then propose a context-based parsing approach that combines efficient statistical learning of deep parse trees with their semantic pruning by type checking and large-theory automated theorem proving. We show that our learning method allows efficient use of large amount of contextual information, which in turn significantly boosts the precision of the statistical parsing and also makes it more efficient. This leads to a large improvement of our first results in parsing theorems from the Flyspeck corpus.

  • Leonardo de Moura (RISE, Microsoft Research)

    Title: Whitebox Automation
    Joint work with Jeremy Avigad, Gabriel Ebner, Jared Roesch, and Sebastian Ullrich

    Abstract: We describe the metaprogramming language currently in use in Lean, a new open source theorem prover that is designed to bridge the gap between interactive use and automation. Lean implements a version of the Calculus of Inductive Constructions. Its elaborator and unification algorithms are designed around the use of type classes, which support algebraic reasoning, programming abstractions, and other generally useful means of expression. Lean also has parallel compilation and checking of proofs, and provides a server mode that supports a continuous compilation and rich user interaction in editing environments such as Emacs, Vim, and Visual Studio Code. Lean currently has a conditional term rewriter, and several components commonly found in state-of-the-art Satisfiability Modulo Theories (SMT) solvers such as forward chaining, congruence closure, handling of associative and commutative operators, and E-matching. All these components are available in the metaprogramming framework, and can be combined and customized by users.

    In this talk, we provide a short introduction to the Lean theorem prover and its metaprogramming framework. We also describe how this framework extends Lean's object language with an API to many of Lean's internal structures and procedures, and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our implementation is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation.

    We view this as important progress towards our overarching goal of bridging the gap between interactive and automated reasoning. Users who develop libraries for interactive use can now more easily develop special-purpose automation to go with them thereby encoding procedural heuristics and expertise alongside factual knowledge. At the same time, users who want to use Lean as a back end to assist in complex verification tasks now have flexible means of adapting Lean's libraries and automation to their specific needs. As a result, our metaprogramming language opens up new opportunities, allowing for more natural and intuitive forms of interactive reasoning, as well as for more flexible and reliable forms of automation.

    More information about Lean can be found at http://leanprover.github.io. The interactive book ``Theorem Proving in Lean'' is the standard reference for Lean. The book is available in PDF and HTML formats. In the HTML version, all examples and exercises can be executed in the reader's web browser.

  • Federal Prosecution Office

    ITP 2017 Accepted Papers

  • Alexander Bentkamp, Jasmin Christian Blanchette and Dietrich Klakow.
    A Formal Proof of the Expressiveness of Deep Learning
  • Luís Cruz-Filipe, Kim S. Larsen and Peter Schneider-Kamp.
    How to Get More Out of Your Oracles
  • Véronique Benzaken and Evelyne Contejean, Stefania Dumbrava.
    Certifying Standard and Stratified Datalog Inference Engines in SSReflect
  • Zhe Hou, David Sanan, Alwen Tiu and Yang Liu.
    Proof Tactics for Assertions in Separation Logic
  • Lorenzo Gheri and Andrei Popescu.
    A Formalized General Theory of Syntax with Bindings
  • Julian Rosemann, Sigurd Schneider and Sebastian Hack.
    Verified Spilling and Translation Validation with Repair
  • Dominique Larchey-Wendling.
    Typing Total Recursive Functions in Coq
  • Marijn Heule, Warren Hunt, Matt Kaufmann and Nathan Wetzler.
    Efficient, Verified Checking of Propositional Proofs
  • Adam Sandberg Ericsson, Magnus O. Myreen and Johannes Åman Pohjola.
    A Verified Generational Garbage Collector for CakeML
  • Bohua Zhan.
    Formalization of the fundamental group in untyped set theory using auto2
  • Sylvie Boldo, Mioara Joldes, Jean-Michel Muller and Valentina Popescu.
    Formal Verification of a Floating-Point Expansion Renormalization Algorithm
  • Andrea Gabrielli and Marco Maggesi.
    Formalizing Basic Quaternionic Analysis
  • Laureano Lambán, Francisco-Jesus Martín-Mateos, Julio Rubio and Jose-Luis Ruiz-Reina.
    Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms
  • Raphaël Cauderlier and Catherine Dubois.
    FoCaLiZe and Dedukti to the Rescue for Proof Interoperability
  • David Butler, David Aspinall and Adria Gascon.
    How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation
  • Andreas Lochbihler.
    Effect polymorphism in higher-order logic (proof pearl)
  • Ulrik Buchholtz, Floris van Doorn and Jakob von Raumer.
    Homotopy Type Theory in Lean
  • Yanni Kouskoulas, Daniel Genin, Aurora Schmidt and Jean-Baptiste Jeannin.
    Formally verified safe vertical maneuvers for non-deterministic, accelerating aircraft dynamics
  • Sophie Bernard.
    Formalization of the Lindemann-Weierstrass theorem
  • Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan and Jan Vitek.
    Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology
  • Frédéric Besson, Sandrine Blazy and Pierre Wilke.
    CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics
  • Yannick Forster and Gert Smolka.
    Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq
  • Nathan Fulton, Stefan Mitsch, Brandon Bohrer and André Platzer.
    Bellerophon: Tactical Theorem Proving for Hybrid Systems
  • Cyril Cohen and Damien Rouhling.
    A Formal Proof in Coq of LaSalle's Invariance Principle
  • Frédéric Gilbert.
    Proof certificates in PVS
  • Myrthe van Delft, Herman Geuvers and Tim Willemse.
    A Formalisation of Consistent Consequence for Boolean Equation Systems
  • Xavier Allamigeon and Ricardo D. Katz.
    A Formalization of Convex Polyhedra based on the Simplex Method
  • Michael Kohlhase, Dennis Müller, Sam Owre, and Florian Rabe.
    Making PVS Accessible to Generic Services by Interpretation in a Universal Format
  • Dirk Pattinson and Mukesh Tiwari.
    Schulze Voting as Evidence Carrying Computation
  • Dominik Kirst and Gert Smolka.
    Categoricity Results for Second-Order ZF in Dependent Type Theory
  • University of Brasilia

    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

    Organisation:

    The conference is organised by the Departments of Computer Science (CIC) and Mathematics (MAT) at the University of Brasília and by the Departments of Informatics and Applied Mathematics (DIMAp) and Mathematics (DMAT) 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

    History

    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

    Traditions

    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

    Workshops:

  • 12th Workshop on 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
    23 and 24 September 2017
  • Tutorials:

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

    Accepted Abstracts: Poster Session

    The Poster Session is scheduled for Thursday 28/09 and will be preceded by short talks, which should be at most 5 minutes long. Posters should have the form A1: 594 x 841 mm (23.4 x 33.1 inches - portrait).

  • Combined Proof Methods For Multimodal K
    Daniella Angelos, Cláudia Nalon
  • Congruence Closure with Free Variables
    Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
  • Conditional Parametricity in Isabelle/HOL
    Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel
  • Mining for Formalization Environments in the Mizar Mathematical Library
    Adam Naumowicz
  • Formal Verification of the Dynamic Authentication Protocol
    Felipe Rodopoulos de Oliveira, Cláudia Nalon
  • On Generalizing Decidable Standard Prefix Classes of First-Order Logic
    Marco Voigt
  • Program Extraction for Mutable Arrays
    Kazuhiko Sakaguchi
  • A resolution-based E-connection calculus
    Lucas Amaral, Cláudia Nalon
  • Automatic Complexity Analysis of Programs
    Florian Frohn, Jürgen Giesl
  • Formal Verification of Smart Contracts
    Chad E. Brown, Ondrej Kuncar Josef Urban
  • Polynomials, rivals of tableaux
    Walter Carnielli
  • Craig Interpolation and Query Reformulation with Clausal First-Order Tableaux
    Christoph Wernhard
  • Mind the Gap: Metric Temporal Logic Translations
    Ullrich Hustadt, Clare Dixon, Ana Ozaki
  • Verified Model Checking of Timed Automata
    Simon Wimmer, Peter Lammich
  • 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 two pages 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 June 20, 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

    Preliminary Programme

    Preliminary Programme

    Keys:
    IT = Invited Talk
    TP = Technical Presentation
    T/F/I = TABLEAUX/FroCoS/ITP
    T1-T4 = tutorials

    Itamaraty Palace

    ITP 2017 Programme

    The programme can be downloaded as a pdf file by clicking here.

    Tuesday, 26th September

    Session 01
    Chair César Muñoz
    ITP Invited Talk
    08:30Whitebox automation
    Leonardo de Moura
    HO Logic and Type Theory
    09:30(T01) Effect polymorphism in higher-order logic (proof pearl)
    Andreas Lochbihler
    10:00(T02) Typing Total Recursive Functions in Coq
    Dominique Larchey-Wendling
    10:30Coffee Break
    Session 02
    Chair Hélène Kirchner
    Security
    11:00(T03) How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation
    David Butler, David Aspinall and Adrià Gascón
    11:30(T04) Schulze Voting as Evidence Carrying Computation
    Dirk Pattinson and Mukesh Tiwari
    12:00(T05)Certifying Standard and Stratified Datalog Inference Engines in SSReflect
    Stefania Dumbrava, Véronique Benzaken and Évelyne Contejean
    12:30Lunch
    Session 03
    Tableaux Invited Talk
    Chair Pascal Fontaine
    14:00Tableau Calculus for Hybrid Xpath with Data
    Carlos Areces
    Chair Luís Cruz-Filipe
    Programming Languages
    15:00(T06) Formal Verification of a Floating-Point Expansion Renormalization Algorithm
    Sylvie Boldo, Mioara Joldes, Jean-Michel Muller and Valentina Popescu
    15:30Coffee Break
    Session 04
    Chair Andreas Lochbihler
    Programming Languages
    16:00(T07) Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology
    Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan and Jan Vitek
    16:30(T08) A Verified Generational Garbage Collector for CakeML
    Adam Sandberg Ericsson, Magnus O. Myreen and Johannes &‌Aring;man Pohjola
    17:00(T09) CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics
    Frédéric Besson, Sandrine Blazy and Pierre Wilke
    17:30(T10) Verified Spilling and Translation Validation with Repair
    Julian Rosemann, Sigurd Schneider and Sebastian Hack

    Wesnesday, 27th September

    Session 05
    Joint Tableaux/Frocos/ITP Invited Talk
    Chair Elaine Pimentel
    08:30The perimeter of decidability (with sequent calculi on the inside)
    Katalin Bimbó
    Chair Adam Naumowicz
    Formalization of Mathematics
    09:30(T11) Formalizing Basic Quaternionic Analysis
    Andrea Gabrielli and Marco Maggesi
    10:00(T12) A Formalization of Convex Polyhedra based on the Simplex Method
    Xavier Allamigeon and Ricardo D. Katz
    10:30Coffee Break
    Session 06
    Chair Mariano Moscato
    Tactics
    11:00(T13) A Formal Proof of the Expressiveness of Deep Learning
    Alexander Bentkamp, Jasmin Christian Blanchette and Dietrich Klakow
    11:30(T14) A Formalisation of Consistent Consequence for Boolean Equation Systems
    Myrthe van Delft, Herman Geuvers and Tim Willemse
    12:00(T15) Proof Tactics for Assertions in Separation Logic
    Zhe Hou, David Sanan, Alwen Tiu and Yang Liu
    12:30Lunch
    Session 07
    Chair Amy Felty
    Joint Tableaux/Frocos/ITP Inv. Talk
    14:00 Automating Formalization by Statistical and Semantic Parsing of Mathematics
    Cezary Kaliszyk
    Tactics
    15:00(T16) Efficient Verified Checking of Propositional Proofs
    Marijn Heule, Warren Hunt, Matt Kaufmann and Nathan Wetzler
    15:30Short Coffee Break
    15:45Excursion
    18:00Dinner

    Thursday, 28th September

    Session 08
    Frocos Invited Talk
    Chair Clare Dixon
    08:30Revising System Specfications in Temporal Logic
    Renata Wassermann
    09:30FLOC 2018 Announcement
    Didier Galmiche, Roberto Sebastiani
    09:45 Poster's Presentation
    Renate A. Schmidt
    10:30Coffee Break, Poster's Display
    Session 09
    Chair Florian Rabe
    Theorem Proving Interoperability
    11:20(T17) FoCaLiZe and Dedukti to the Rescue for Proof Interoperability
    Raphaël Cauderlier and Catherine Dubois
    11:50(T18) Proof certificates in PVS (Rough Diamond)
    Frédéric Gilbert
    12:10(T19) How to Get More Out of Your Oracles (Rough Diamond)
    Luís Cruz-Filipe, Kim S. Larsen and Peter Schneider-Kamp
    12:30Lunch
    Session 10
    Joint Tableaux/Frocos/ITP Invited Talk
    Chair Marcelo Finger
    14:00Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
    Jasmin Blanchette
    Chair David Aspinall
    Theorem Proving Interoperability
    15:00(T20) Making PVS Accessible to Generic Services by Interpretation in a Universal Format
    Michael Kohlhase, Dennis Müller, Sam Owre and Florian Rabe
    15:30Coffee Break
    Session 11
    Chair Flávio de Moura
    HO Logic and Type Theory
    16:00(T21) A Formalized General Theory of Syntax with Bindings
    Lorenzo Gheri and Andrei Popescu
    16:30 (T22) Categoricity Results for Second-Order ZF in Dependent Type Theory
    Dominik Kirst and Gert Smolka
    17:00Business Meeting
    Jens Otten, Franz Baader, César Munõz

    Friday, 29th September

    Session 12
    Chair Mauricio Ayala-Rincón
    ITP Invited Talk
    08:30 Automated Theory Exploration for Interactive Theorem Proving: An introduction to the Hipster system
    Moa Johansson
    (Sponsored by the European Association for Artificial Intelligence - EurAI)
    HO Logic and Type Theory
    09:30(T23) Homotopy Type Theory in Lean
    Floris van Doorn, Jakob von Raumer and Ulrik Buchholtz
    10:00(T24) Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq
    Yannick Forster and Gert Smolka
    10:30Coffee Break
    Session 13
    Chair Sam Owre
    Engineering Applications
    11:00 (T25) Formally Verified Safe Vertical Maneuvers for Non-Deterministic, Accelerating Aircraft Dynamics
    Yanni Kouskoulas, Daniel Genin, Aurora Schmidt and Jean-Baptiste Jeannin
    11:30(T26) Bellerophon: Tactical Theorem Proving for Hybrid Systems
    Nathan Fulton, Stefan Mitsch, Brandon Bohrer and André Platzer
    12:00(T27) A Formal Proof in Coq of LaSalle's Invariance Principle
    Cyril Cohen and Damien Rouhling
    12:30Lunch
    Session 14
    Frocos Invited Talk
    14:00 Designing Extensible Theory Solvers
    Cesare Tinelli
    Chair Catherine Dubois
    Formalization of Mathematics
    15:00(T28) Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms
    Laureano Lambán, Francisco-Jesus Martín-Mateos, Julio Rubio and José-Luis Ruiz-Reina
    15:30Coffee Break
    Session 15
    Chair José-Luis Ruiz-Reina
    Formalization of Mathematics
    16:00(T29) Formalization of the Lindemann-Weierstrass theorem
    Sophie Bernard
    16:30(T30) Formalization of the fundamental group in untyped set theory using auto2
    Bohua Zhan
    17:00Closing
    Itamaraty Palace

    Grants and Financial Support

    Students Grants

    A limited number of travel grants is available for students who would not otherwise have resources to attend TABLEAUX/FroCoS/ITP, and whose attendance would benefit both the applicant and the event. We expect to be able to help with local/travel expenses up to 250 EUR per student. Applicants should note that grants are limited, and that costs in excess of the grant will not be reimbursed.

    Grants will be awarded based on the grant committee's assessment of the applicant's genuine financial need, the potential benefit to the applicant's education and research, and the potential benefit to TABLEAUX/FroCoS/ITP. Among those applicants who genuinely could not attend TABLEAUX/FroCoS/ITP without a grant, the evaluating committee gives priority to (co-)authors of accepted papers.

    Although priority is given to students with active role in the conferences/workshops, students in other situations are very much encouraged to apply.

    Applications should explain briefly (limited to 2000 characters)

    • the current status of the applicant
    • the kind of participation of the applicant in TABLEAUX/FroCoS/ITP
    • a breakdown of the estimated amount needed

    Applications should be sent by August 10th 2017 by email to Elaine Pimentel (elaine.pimentel at gmail.com). Students should have their supervisor sent a brief recommendation email (limited to 2000 characters) to the same address and by the same deadline. This letter should describe the student's work, the benefit to that work of attending the conference, and an assessment of the student's financial need.

    The award notification date is August 15th, 2017.

    The grants will be presented at the conferences; in case a grantee does not attend, the chairs may transfer the grant to another student or give no award.

    The grants are offered by Springer and by the organisation of the conferences.

    For more information please contact the local organisers:

    • Elaine Pimentel (elaine.pimentel at gmail.com)
    • Daniele Nantes (daniele.nantes at gmail.com)

    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

    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

    Registration

    The registration page is no longer available (2017-10-18). Early registration is until the 4th August. Late registration until the 2nd September. After that, registration can be done only on the venue at the same prices of late registration, but only payment in cash can be taken. All prices are all given in Brazilian Reals. Regular fees include coffee breaks, lunchs, proceedings of the selected conferences/workshops, and social activities. Student fees include coffee breaks, lunchs, proceedings of the selected conferences/workshops, but do not include social activities (excursion/dinner).

    Early Registration (until 4th August 11th August)

    Conferences: TABLEAUX, FroCoS, ITP

  • One conference only: R$ 1065.00 (regular), R$ 760.00 (student)
  • Any two conferences: R$ 1255.00 (regular), R$ 855.00 (student)
  • All three conferences: R$ 1445.00 (regular), R$ 950.00 (student)
  • Workshops:

  • LSFA 2017: R$ 495.00 (regular), R$ 325.00 (student)
  • PxTP 2017: R$ 345.00 (regular), R$ 230.00 (student)
  • EPS: R$ 230.00 (regular), R$ 155.00 (student)
  • Dalí: R$ 460.00 (regular), R$ 310.00 (student)
  • Tutorials

  • Each: R$ 230.00 (regular), R$ 155.00 (student)
  • Late Registration (until 2nd September)

    Conferences: TABLEAUX, FroCoS, ITP

  • One conference only: R$ 1280.00 (regular), R$ 915.00 R$ 760.00 (student)
  • Any two conferences: R$ 1510.00 (regular), R$ 1030.00 R$ 855.00 (student)
  • All three conferences: R$ 1735.00 (regular), R$ 1140.00 R$ 950.00 (student)
  • Workshops:

  • LSFA 2017: R$ 595.00 (regular), R$ 390.00 R$ 325.00 (student)
  • PxTP 2017: R$ 415.00 (regular), R$ 280.00 R$ 230.00 (student)
  • EPS: R$ 280.00 (regular), 190.00 R$ 155.00 (student)
  • Dalí: R$ 560.00 (regular), R$ 380.00 R$ 310.00 (student)
  • Tutorials

  • Each: R$ 280.00 (regular), R$ 190.00 R$ 155.00 (student)
  • Extras (any time)

  • Extra tickets excursion/conference dinner: R$ 380.00
  • Physical copy of the EPS: R$ 80.00
  • Ipê Amarelo

    Venue

    All the events will be held at the Finatec building located within the University of Brasília.
    Finatec- Fundação de Empreendimentos Científicos e Tecnológicos
    Campus Universitário Darcy Ribeiro
    Av. L3 Norte, Ed. Finatec
    Asa Norte, Brasília – DF
    CEP 70910-900
    Tel.: +55 61 3348 0400

    Local Information:

    (This is under construction. Please return for more information.)

    Accessibility

    Brasília is served by an international airport which handles around 19 million passengers a year. As part of the preparation for hosting the 2014 FIFA World Cup, the airport received massive investments, from both the public and private sectors, for the renovation of the passenger’s terminals and the enlargement of the taxiways, which has allowed to almost double the number of positions available for aircrafts and, thus, increase the number of available routes for both domestic and international flights. International flights directly connect Brasília with Santiago (Chile), Panama City (Panama), Miami (USA), Atlanta (USA), and Lisbon (Portugal).

    It is also worthy mentioning that Brasília hosts one of the most important regional hubs in Brazil. There are direct flights from all the state capitals, including Rio de Janeiro, São Paulo, Porto Alegre, Natal, Recife, among other places which are easily accessible directly from other continents and from other countries in the Americas.

    Brasília is centrally located and well served by coaches from elsewhere in Brazil, but prices for internal flights are competitive and travel times much shorter.

    Transportation

    The airport is just 20 minutes away from the centre, where the hotels are. Taxis cost around € 15.00 and are a convenient way to go from and to the airport.

    There is also an Executive Bus from the airport to the Hotels Sectors. It runs every half an hour and stops by the door of or conveniently close to the main hotels in these areas. The trip costs R$ 12.00 (around € 2.50).

    Regular buses (lines 102, 102.1) also run from the airport to the main bus terminal in town, are frequent and quite cheap (€ 0.50). From the bus terminal you will need to catch another bus or a taxi to get to other places. If you do not speak Portuguese or do not know your way around, this is not recommended for you.

    Visa Requirements

    Brazil’s foreign policy is based on reciprocity. The Brazilian immigration authority will not require application for a visa prior to travelling/entering the country if your own country does not require such from Brazilian nationals. Nationals of 86 countries can enter Brazil without a visa, including all EU countries. For those who need a visa, there is a special category for attendees of scientific meetings (VITUR), where a letter of invitation is needed. You should check with the Brazilian Consulate in your country what the requirements are. The organisation of the event will provide the required letters upon registration, in case you need them to apply for visas.

    Accommodation

    Brasília has a vast number of hotels. They are located in the central area, closer to the cross between the Monumental and the Residential Axes, about 10 minutes by car to the events venue.

    We have negotiated special rates at the Comfort Suítes Brasília:

  • Single: R$ 237,00
  • Double: R$ 280,00
  • Values are per night, breakfast is included, and taxes are not included (15%). In order to benefit from these rates, you need to contact the hotel directly via email (reservas.csb@atlanticahotels.com.br or eventos.csb@atlanticahotels.com.br) and cite the conferences.

    Alternatives can be found at the usual search sites: Booking.com, airbnb, Trip Advisor, etc.

    Shuttle Hotels/FINATEC/Social Events

    The organisation will provide transportation from the North Hotels Sector (SHN, stop in front of the Comfort Suítes Brasíllia) to the FINATEC Building at the University of Brasília (UnB). The trips between UnB (ICC Norte) and UnB (Finatec) are for registered attendees of the tutorial "PVS for Computer Scientists". We will also provide transportation from the Finatec Building to the Itamaraty Palace, and from there to the APCEF (where the dinner will be held).

    • 23/09/17
      • 07:40:00 SHN ↦ UnB (Finatec)
      • 08:15:00 SHN ↦ UnB (Finatec)
      • 17:45:00 UnB (Finatec) ↦ SHN
      • 18:00:00 UnB (Finatec) ↦ SHN
    • 24/09/17
      • 07:50:00 SHN ↦ UnB (Finatec)
      • 08:15:00 SHN ↦ UnB (Finatec)
      • 17:00:00 UnB (Finatec) ↦ SHN
      • 17:30:00 UnB (Finatec) ↦ SHN
    • 25/09/17
      • 07:40:00 SHN ↦ UnB (Finatec)
      • 08:10:00 UnB (Finatec) ↦UnB (ICC Norte)
      • 11:30:00 SHN ↦ UnB (Finatec)
      • 12:30:00 UnB (ICC Norte) ↦ UnB (Finatec)
      • 13:50:00 UnB (Finatec) ↦UnB (ICC Norte)
      • 17:30:00 UnB (ICC Norte) ↦ UnB (Finatec)
      • 18:00:00 UnB (Finatec) ↦ SHN
      • 18:30:00 UnB (Finatec) ↦ SHN
    • 26/09/17
      • 07:30:00 SHN ↦ UnB (Finatec)
      • 08:00:00 SHN ↦ UnB (Finatec)
      • 18:00:00 UnB (Finatec) ↦ SHN
      • 18:30:00 UnB (Finatec) ↦ SHN
    • 27/09/17
      • 07:00:00 SHN ↦ UnB (Finatec)
      • 07:30:00 SHN ↦ UnB (Finatec)
      • 08:00:00 SHN ↦ UnB (Finatec)
      • 15:40:00 UnB (Finatec) ↦Itamaraty
      • 16:10:00 UnB (Finatec) ↦ SHN
      • 16:40:00 UnB (Finatec) ↦ Itamaraty
      • 17:00:00 Itamaraty ↦ APCEF
      • 18:00:00 Itamaraty ↦ APCEF
      • 21:00:00 APCEF ↦ SHN
      • 21:30:00 APCEF ↦ SHN
      • 22:00:00 APCEF ↦ SHN
    • 28/09/17
      • 07:00:00 SHN ↦ UnB (Finatec)
      • 07:30:00 SHN ↦ UnB (Finatec)
      • 08:00:00 SHN ↦ UnB (Finatec)
      • 17:20:00 UnB (Finatec) ↦ SHN
      • 17:50:00 UnB (Finatec) ↦ SHN
      • 18:30:00 UnB (Finatec) ↦ SHN
    • 29/09/17
      • 07:30:00 SHN ↦ UnB (Finatec)
      • 08:00:00 SHN ↦ UnB (Finatec)
      • 17:15:00 UnB (Finatec) ↦ SHN
      • 17:40:00 UnB (Finatec) ↦ SHN

    Vaccination

    Brazil does not require an International Certificate of Vaccination or Prophylaxis for entry into the country.

    Travelers are encouraged, however, to ensure their routine immunizations are up to date (as recommended by their country of origin), since it is an effective and safe measure for the prevention of various diseases.

    Brasília is not in the endemic area of yellow fever. However, it is also important that travellers take yellow fever vaccination 10 days before visiting forested areas or participating in ecotourism or rural tourism activities. For further information on yellow fever, please click here.

    (source: Brazilian Ministry of Health)

    Out and Around

    Brasília is a modern, lively place, with a variety of attractions worth seeing. For those who like the urban environment and cultural activities, almost all public buildings are open for visitation, most of them with free guided tours. Besides the architectural features, they hold interesting art collections which are also open for visitation. For the more adventurous, we are in the middle of the Cerrado ecosystem, which makes trips to nearby parks and waterfalls a very pleasant experience. Some of the suggested places to visit include the National parks:

    and nearby cities of historical interest:

    National Congress

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