Developing formal methods to program and reason about infinite data types, whether they are inductive or coinductive, is challenging and subject to numerous recent research efforts.
Often approached in rather ad hoc ways in the past decades, the understanding of the logical and computational principles underlying those programming phenomena is reaching a more mature stage as proved by the many advances published in the recent years.
Various examples of this can be viewed in recent works on co-patterns, infinite proof systems for logics with fixed points, circular proofs, guarded recursive type theory, the treatment of coinduction in proof assistants, concrete semantics of coinductive computation, recent methods in infinitary rewriting, or the extension of the Curry-Howard correspondence to linear temporal logic and functional reactive programming to name as few.
The workshop aims at gathering researchers working on those topics
as well as colleagues interested in understanding those recent
results and open problems of this line of research.
For outsiders, the workshop will offer tutorial sessions and
survey-like invited talks.
For specialists of the topic, the workshop will permit to
gather people working with syntactical or semantical methods,
people focusing on proof systems or programming languages,
foster exchanges and discussions benefiting from their
Type systems: infinitary type systems, guarded recursive type theory, ...
Curry-Howard correspondence to linear temporal logic and functional reactive programming.
Semantics: denotational and interactive semantics for infinite data and computations
Tools: extensions of programming languages and proof assistants to better trat with infinite data; results on extending programming languages with primitives for manipulating infinite data such as streams in a more structured and convenient way; coinductive proof methods in proof assistants
Proof theory and model-checking: Additionally, the workshop will welcome works demonstrating how proof-theoretical investigations can be applied to model-checking problems.