WAIT 2018

Fourth International Workshop on Automated (Co)inductive Theorem Proving

28–29 June 2018, Amsterdam, The Netherlands
Co-located with Matryoshka 2018

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 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

Welcome

09:05 – 09:45

Tree Grammars for Induction on Inductive Data Types modulo Equational Theories
Gabriel Ebner
Joint work with Stefan Hetzl
(slides)

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)
Nicholas Smallbone
(slides)

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.

Coffee break

Session 2 (chair: Stefan Hetzl)

11:00 – 11:45

SMT-LIB 3: Bringing Higher-Order Logic to SMT
Pascal Fontaine
Joint work with Clark Barrett and Cesare Tinelli
(slides)

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.

Clark Barrett, Pascal Fontaine and Cesare Tinelli are the current SMT-LIB managers and are co-authors of this presentation (but Pascal will take all the blame for mistakes, e.g. misunderstanding TIP features).

11:45 – 12:30

An Induction Principle for Automated Induction
Koen Claessen
Joint work with Linnea Andersson and Andres Wahlström
(slides) (link)

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
Moa Johansson
(slides)

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
Sólrún Halla Einarsdóttir
Joint work with Moa Johansson and Johannes Åman Pohjola
(slides)

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
Henning Basold

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

Mechanically Certifying Formula-Based Noetherian Induction Reasoning
Sorin Stratulat
(slides)

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

What Are the Suitable Data Types for Syntax with Bindings?
Andrei Popescu
Joint work with Jasmin Blanchette, Lorenzo Gheri, and Dmitriy Traytel
(slides)

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

Wrap-up

19:30 –

Workshop dinner
Rozengeur (Iranian cuisine)


Friday 29 June
 

Session 5 (chair: Henning Basold)

09:00 – 09:45

Towards Coinductive Theory Exploration in Horn Clause Logic
Ekaterina Komendantskaya
(slides)

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

Finite and Infinite Traces, Inductively and Coinductively
Jurriaan Rot
(slides)

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.

Coffee break

Session 6 (chair: Sorin Stratulat)

11:00 – 11:45

Cyclic Superposition and Induction
Jannik Vierling
(slides)

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

Superposition with Datatypes and Codatatypes
Simon Robillard
Joint work with Jasmin Blanchette and Nicolas Peltier
(slides)

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.

Lunch break

Session 7 (chair: Jasmin Blanchette)

14:00 – 14:30

Friendly Corecursion in Isabelle/HOL
Andrei Popescu
Joint work with Jasmin Blanchette, Aymeric Bouzy, Andreas Lochbihler, and Dmitriy Traytel
(slides)

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

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* (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)

* speakers

Jasmin Blanchette (VU Amsterdam)
Johannes Hölzl (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. 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.