Fourth International Workshop on Automated (Co)inductive Theorem Proving
28–29 June 2018, Amsterdam, The Netherlands
Inductive and coinductive theorem proving is a topic of growing interest in the automated reasoning community. The Fourth International Workshop on Automated (Co)inductive Theorem Proving (WAIT 2018) focuses on all relevant aspects of (co)inductive reasoning.
The workshop is an informal event and aims to give researchers interested in the topic a chance to meet, exchange ideas, and have a platform for discussions.
We invite talks featuring demonstrations and tutorials of (co)inductive theorem provers, challenge problems, new directions of research, or anything else of interest to the (co)inductive theorem proving community.
Please send an email to the organizers if you would like to give a talk, demonstrate a tool, or otherwise participate.
The workshop will take place on 28 and 29 June 2018 in the main building of the Vrije Universiteit Amsterdam, room Agora 3. The VU is easily accessible on foot from the Amsterdam Zuid station, a short train ride away from Amsterdam Airport Schiphol. There are also parking spaces. See How to get to VU Amsterdam for details. The workshop will start on 28 June at 09:00 and end on 29 June at 15:00.
WAIT 2018 will take place the same week as the First European Workshop on Higher-Order Automated Reasoning (Matryoshka 2018).
Hotels in Amsterdam can be very expensive. Even the cheapest options often cost over 100 euros per night. The neighboring city of Amstelveen has more reasonably priced options (e.g., Ibis) and is located close to the VU campus, a few stops away by public transportation (tram line 5 or metro line 51).
Thursday 28 June
Session 1 (chair: Johannes Hölzl)
|09:00 – 09:05|
|09:05 – 09:45||
Inductive theorem proving based on tree grammars was introduced by Eberhard and Hetzl in 2015. In this approach, proofs with induction on natural numbers are found by generalizing automatically generated proofs of finite instances on the level of Herbrand disjunctions. We extend this method to support general inductive data types, and reasoning modulo a background theory to abstract from irregularities in automatically generated proofs. We present an experimental implementation of the method and show that it automatically produces non-analytic induction formulas for several examples.
|09:45 – 10:30||
Finding Loop Invariants with QuickSpec (Work in Progress)
Recently I've been playing with using QuickSpec on imperative programs to discover loop invariants and similar assertions. I will talk about how I do it, as well as a crazy idea you can implement on top of it: psychic property-based testing.
Session 2 (chair: Stefan Hetzl)
|11:00 – 11:45||
I will first present the recent advances in SMT-LIB, and the future
directions. I will also review the TIP format, and quickly discuss the
features that have been imported into SMT-LIB, and those that aren't
yet. We (the SMT-LIB managers) are keen to get input and feedback from
the community, so I will be happy if the talk quickly becomes an open
discussion about the nice features you want, the restrictions you
hate, and get suggestions to make SMT-LIB an even more solid, clean,
and clear standard for your problems.
|11:45 – 12:30||
An Induction Principle for Automated Induction
We explore alternatives to structural induction for use in automated induction. Our main candidate is a generalization of recursion induction.
Session 3 (chair: Andrei Popescu)
|14:00 – 14:45||
I will give a brief introduction to the theory exploration system Hipster, which discovers and proves lemmas by induction automatically. There will be a simple demo on some small examples, followed by a more speculative part where I'll invite to discussion on what is needed to make theory exploration tools efficient, stable and general enough to be of real use in e.g. a proof assistant.
|14:45 – 15:30||
We have extended theory exploration to discover coinductive lemmas about corecursive (co)datatypes and functions. This required new methods for testing infinite values and for automated coinductive proofs. Our extension has been implemented in the Hipster theory exploration system for the proof assistant Isabelle/HOL.
Session 4 (chair: Ekaterina Komendantskaya)
|16:00 – 16:40||
Recursive Proofs for Coinductive Predicates
We will discuss in this talk how to extend logics with the so-called later modality, which allows us to construct recursive proofs for arbitrary coinductive predicates. The later modality enables goal-directed proof discovery and the use any up-to technique that is provably compatible in the underlying logic. Often, we find that the resulting proof system also admits induction, either because of the nature of the coinductive predicate or through an up-to technique.
|16:40 – 17:10||
I describe general formal tools for certifying formula-based Noetherian induction proofs by Coq, then show how to apply them to certify cyclic proofs of conjectures about conditional specifications. The certification methodology can be easily adapted to automatically certify proofs built with a reductive rewrite-based inference system and, more generally, any formula-based Noetherian induction reasoning.
|17:10 – 17:40||
Syntax with bindings is notoriously difficult to formalize and reason about in proof assistants. A main cause for this is the difficulty to characterize syntax with bindings by means of abstract data types in a useful way, so as to provide high-level structural induction and recursion principles. I will discuss some approaches to address this problem, including a recent line of work pursued in Isabelle/HOL together with colleagues.
|17:40 – 18:00||
Session 5 (chair: Henning Basold)
|09:00 – 09:45||
Coinduction occurs in two guises in Horn clause logic: in proofs of self-referencing properties and relations, and in proofs involving construction of infinite data. Both instances of coinductive reasoning appeared in the literature before, but a systematic analysis of these two kinds of proofs and of their relation was lacking. We propose a general proof-theoretic framework for handling both kinds of coinduction arising in Horn clause logic. To this aim, we propose a coinductive extension of Miller et al’s framework of uniform proofs which we then use as a machinery for formulating and proving coinductive invariants required in proofs with first-order Horn clause logic.
09:45 – 10:30
It is a well-known fact (used e.g. in model checking) that, on finitely branching transition systems, finite trace equivalence coincides with infinite trace equivalence. I will show how to prove this coinductively, which is arguably nicer than the standard inductive proof.
Session 6 (chair: Sorin Stratulat)
|11:00 – 11:45||
In 2013 Kersani and Peltier introduced the n-clause calculus, a superposition calculus enriched with a cycle detection rule realizing a form of reasoning by mathematical induction. Until now it is not known which form of induction is captured by the n-clause calculus. An upper bound in terms of the quantifier complexity of the induction invariant can be obtained by a two step translation: in a first step we encode cyclic refutations in a cyclic sequent calculus introduced by Brotherston and Simpson in 2010; in a second step we translate cyclic proofs into inductive LK proofs.
|11:45 – 12:30||
The absence of a finite axiomatization of the first-order theory of datatypes and codatatypes represents a challenge for automatic theorem provers. We present two approaches to reason by saturation in this theory: one is a conservative theory extension with a finite number of axioms; the other is an extension of the superposition calculus, in conjunction with axioms.
Session 7 (chair: Jasmin Blanchette)
|14:00 – 14:30||
Corecursion is a mechanism for defining functions that produce infinite objects such as streams, lazy lists and infinite-depth trees. Establishing corecursion schemes that are expressive, sound and automatic is a notoriously hard problem. I will discuss an approach, implemented in the proof assistant Isabelle/HOL, for training a logical system to learn stronger and stronger schemes on a sound basis. The central notion is that of a friendly operator (or friend), which constitutes a statically safe context for corecursive calls. The framework relies on the ability to recognize friends quasi-automatically by verifying relational parametricity conditions. I will also discuss some ideas on how to go beyond statically safe contexts with the price of mild dynamic checks.
|14:30 – 15:00||
Maximilian Algehed (Chalmers Gothenburg)
Henning Basold* (ENS Lyon)
Alexander Bentkamp (VU Amsterdam)
Jasmin Blanchette (VU Amsterdam)
Maria Paola Bonacina (U. Verona)
Koen Claessen* (Chalmers Gothenburg)
Martin Desharnais (LMU München)
Gabriel Ebner* (TU Wien)
Sólrún Halla Einarsdóttir* (Chalmers Gothenburg)
Daniel El Ouraoui (U. Lorraine and Inria Nancy)
Pascal Fontaine* (U. Lorraine)
Stefan Hetzl (TU Wien)
Johannes Hölzl (VU Amsterdam)
Moa Johansson* (Chalmers Gothenburg)
Ekaterina Komendantskaya* (Heriot-Watt U.)
Pablo Le Hénaff (École Polytechnique Paris)
Robert Y. Lewis (VU Amsterdam)
Andrei Popescu** (Middlesex U.)
Femke van Raamsdonk (VU Amsterdam)
Martin Riener (U. Manchester)
Simon Robillard* (Chalmers Gothenburg)
Jurriaan Rot* (RU Nijmegen)
Hans-Jörg Schurr (U. Lorraine and Inria Nancy)
Nicholas Smallbone* (Chalmers Gothenburg)
Sorin Stratulat* (U. Lorraine)
Jannik Vierling* (TU Wien)
Petar Vukmirović (VU Amsterdam)
Acknowledgment: We want to thank Pascal Fontaine, Mojca Lovrencak,
and Caroline Waij for helping with the organization.
This workshop is partially supported by the ERC Starting Grant 2016 Matryoshka (grant agreement No.
and by the NWO incidentele steun scheme.
We kindly ask participants to mention the support from the ERC and the NWO
in publications or in other kinds of scientific output that directly follows
from the workshop. (The NWO would also like to receive a copy of the relevant
|This project has received funding from the European Union's Horizon 2020 research and innovation program under grant agreement No. 713999.|