This workshop will take place 19 April 2018, 10:00 room in LIN 1 in the Linaeus building before the defence of my thesis. More details can be found below.

Registration

If you want to attend the workshop, then I would kindly ask you to register. To prevent spam, no direkt link to the registration is provided here. The website for the registration can be reached by replacing workshop.html by registration.html in the address of this website.

Description

Induction and coinduction are two complementary techniques used in mathematics and computer science. These techniques occur together, for example, in control systems: On the one hand, control systems are expected to run until turned off and to always react to their environment. This is what we call coinductive computations. On the other hand, they have to make internal computations. Restricting these computations to terminating, that is inductive, computations ensures that the systems continue to react to their environment. But there are many more applications for mixed inductive-coinductive reasoning, like bialgebras, Brouwer’s fan theorem, continuous functions on coinductive types, Kőnig’s lemma, resolution for coinductive logic programs, recursion theory and weak bisimilarity.

The aim of this one-day workshop is to discuss how inductive-coinductive reasoning is used so far, what techniques exist and how we can advance on those techniques.

Programme

The workshop will take place in room LIN 1 in the Linaeus building, Heyendaalseweg 137 in Nijmegen. During the workshop, coffee and lunch will be served inside the building.

The (preliminary) programme consists of six sessions, as indicated in the following overview.

Abstracts

Coinduction in Uniform

Ekaterina Komendantskaya, Heriot-Watt University

In Chapter 5 of Henning’s thesis, we find a formulation of coinductive variant of first-order intuitionistic logic, named FOL▶. This logic is suggested as a suitable framework for proofs of equality (bisimulation) between infinite streams. The core of this coinductive extension is the Löb rule, originating in the provability logic.

At the same time, my PhD student Yue Li and I have recently proposed a coinductive extension to uniform proofs. Uniform proofs, too, are known for being a fragment of intuitionistic logic. They are a family of proof calculi formulated by Dale Miller et al. for proofs in Horn clause/Hereditary Harrop clause logics. Similarly to Henning’s logic FOL▶, our coinductive extension is based upon one additional coinductive rule COFIX (that however, differs from the Löb rule). Again in line with Henning’s thesis, the motivation behind the coinductive uniform proofs is to provide a general proof-theoretic framework for proofs of coinductive properties of theories (in our case, expressed in Horn Clause logic).

In this talk, I will show connections between these two recently proposed logics; and in particular I will compare the properties of the Löb rule of Henning’s logic and the COFIX rule of the coinductive uniform proofs.

Abstract Rule Formats for Coinductive Operations

Jurriaan Rot, Radboud University

On the Syntax and Semantics of Quantitative Typing

*Andreas Abel, Chalmers University of Technology and Gothenburg University

Quantitative typing generalizes ordinary, linear and affine typing and well-known program analyses such as strictness and dead code detection. Recently, Conor McBride and Bob Atkey have each presented dependent quantitative type theories that properly integrate linearity and dependency. In this talk, I will present my own version of quantitative type theory and discuss its semantics. I will also touch on potential applications, such as free theorems from linearity. This is very much work in progress.

TBA

Tarmo Uustalu, Tallinn University of Technology

TBA

Homotopy Type Theory with Explicit Conversions

Benno van den Berg, University of Amsterdam

Much recent work in type theory, and in homotopy type theory (HoTT) especially, concerns equality. Martin-Löf’s Type Theory has two kinds of equality: judgmental (also: definitional) and propositional. HoTT starts from a novel interpretation of propositional equality as a space of paths and has lead to a much better understanding of propositional equality. In this talk I will argue that one thing that recent work in HoTT has shown, is that it is feasible to completely eliminate judgmental equality in favour of propositional equality and state all computation rule as propositional equalities. In this talk, I wish to present such a purely propositional type theory, reminiscent of “A Logical Framework with Explicit Conversions” by Geuvers and Wiedijk, and discuss its properties (some of which will probably still be in the form of conjectures, as this is still very much work in progress).

Inductive-Coinductive Reasoning: Past and Future

Henning Basold, ENS Lyon, CNRS

In this talk, I will give a brief overview over what the status of mixed inductive-coinductive reasoning is, what we are able to do with ease and what we should be able to do. Just like my thesis, this overview will focus on properties that shall be automatically verified by computers, like static correctness properties of programs and the correctness of mathematical proofs.