
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.
The previous events in the series were hosted in London, Gothenburg, and Vienna. This fourth installment explicitly generalizes the scope to include coinductive methods.
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 HigherOrder 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  Welcome 
09:05 – 09:45 
Tree Grammars for Induction on Inductive Data Types modulo Equational Theories 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 nonanalytic 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 propertybased testing. 
Coffee break  
Session 2 (chair: Stefan Hetzl)  
11:00 – 11:45 
SMTLIB 3: Bringing HigherOrder Logic to SMT
I will first present the recent advances in SMTLIB, and the future
directions. I will also review the TIP format, and quickly discuss the
features that have been imported into SMTLIB, and those that aren't
yet. We (the SMTLIB 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 SMTLIB 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. 
Lunch break  
Session 3 (chair: Andrei Popescu)  
14:00 – 14:45 
Putting Theory Exploration to Work 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 
Theory Exploration for Coinduction 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. 
Coffee break  
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 socalled later modality, which allows us to construct recursive proofs for arbitrary coinductive predicates. The later modality enables goaldirected proof discovery and the use any upto 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 upto technique. 
16:40 – 17:10 
Mechanically Certifying FormulaBased Noetherian Induction Reasoning I describe general formal tools for certifying formulabased 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 rewritebased inference system and, more generally, any formulabased Noetherian induction reasoning. 
17:10 – 17:40 
What Are the Suitable Data Types for Syntax with Bindings? 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 highlevel 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 
Wrapup 
19:30 –  Workshop dinner 


Session 5 (chair: Henning Basold)  
09:00 – 09:45 
Towards Coinductive Theory Exploration in Horn Clause Logic Coinduction occurs in two guises in Horn clause logic: in proofs of selfreferencing 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 prooftheoretic 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 firstorder Horn clause logic. 
09:45 – 10:30 
Finite and Infinite Traces, Inductively and Coinductively It is a wellknown 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. 
Coffee break  
Session 6 (chair: Sorin Stratulat)  
11:00 – 11:45 
Cyclic Superposition and Induction In 2013 Kersani and Peltier introduced the nclause 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 nclause 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 
Superposition with Datatypes and Codatatypes The absence of a finite axiomatization of the firstorder 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. 
Lunch break  
Session 7 (chair: Jasmin Blanchette)  
14:00 – 14:30 
Friendly Corecursion in Isabelle/HOL Corecursion is a mechanism for defining functions that produce infinite objects such as streams, lazy lists and infinitedepth 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 quasiautomatically 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 
Discussion 
Coffee break 
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* (HeriotWatt 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)
HansJörg Schurr (U. Lorraine and Inria Nancy)
Nicholas Smallbone* (Chalmers Gothenburg)
Sorin Stratulat* (U. Lorraine)
Jannik Vierling* (TU Wien)
Petar Vukmirović (VU Amsterdam)
* speakers
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.
713999)
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
publications.)
This project has received funding from the European Union's Horizon 2020 research and innovation program under grant agreement No. 713999. 