PARIS 2018 - Programming And Reasoning on Infinite Structures (PARIS)

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 various perspectives.