<div dir="ltr"><br>Programming And Reasoning on Infinite Structures<br>A workshop affiliated with FSCD@FLOC 2018<br>July 7&8, 2018<br>Oxford, UK<br><br><br>Developing formal methods to program and reason about infinite data,<br>whether inductive or coinductive, is challenging and subject to<br>numerous recent research efforts. The understanding of the logical<br>and computational principles underlying these notions is reaching<br>a mature stage as illustrated by the numerous advances that have<br>appeared in the recent years.<br><br>Various examples of this can be viewed in recent works on co-patterns,<br>infinite proof systems for logics with induction and coinduction,<br>circular proofs, guarded recursive type theory, research effort on<br>integrated coinduction in proof assistants, concrete semantics of<br>coinductive computation, recent developments in infinitary rewriting,<br>or the unveiling of the Curry-Howard correspondence between temporal<br>logics and functional reactive programming, to name a few.<br><br>The workshop aims at gathering researchers working on these topics<br>as well as colleagues interested in understanding the recent results<br>and open problems of this line of research:<br><br>- For outsiders, the workshop will offer tutorial sessions and<br>  survey-like invited talks.<br><br>- For specialists of the topic, the workshop will permit to gather<br>  people working with syntactical or semantical methods, people<br>  focusing on proof systems or programming languages, and foster<br>  exchanges and discussions benefiting from their various<br>  perspectives.<br><br>We are seeking for short submissions (~3-4 pages long) presenting<br>(i) new completed results<br>(ii) work in progress, or<br>(iii) advertising recently published results. <br><br><br>The workshop is affiliated with FSCD 2018, as part of the<br>Federated Logic Conference of 2018 and is funded by French ANR,<br>RAPIDO project.<br><br><br>** Important dates and submission details:<br><br>Submissions: April 15<br>Notification: May 15<br>Final abstract: May 25<br>Workshop: July 7 and 8<br><br>Submission page: <a href="http://easychair.org/conferences/?conf=paris18">http://easychair.org/conferences/?conf=paris18</a><br><br>Website: <a href="https://www.irif.fr/~saurin/RAPIDO/PARIS-2018/">https://www.irif.fr/~saurin/RAPIDO/PARIS-2018/</a><br><br><br>** Program Committee:<br><br>Andreas Abel     (Gothenburg University)<br>David Baelde     (LSV, ENS Paris-Saclay & Inria Paris; co-chair)<br>Amina Doumane    (LIP, ENS Lyon)<br>Martin Lange     (University of Kassel)<br>Rasmus Møgelberg (IT University of Copenhagen)<br>Luke Ong         (University of Oxford)<br>Andrew Polonsky  (Appalachian State University)<br>Colin Riba       (LIP, ENS Lyon)<br>Alexis Saurin    (IRIF, Université Paris Diderot; co-chair)<br>Alex Simpson     (University of Ljubljana)<br><br><br>** Invited speakers:<br><br>A tutorial and two invited talks will be announced shortly.<br><br><br>** Topics:<br><br>Suggested, but not exclusive, topics of interest for the workshop are:<br><br>- Proof systems: proof system for logics with least and greatest fixed<br>  points, infinitary and cyclic/circular proof systems<br><br>- Calculi: infinitary rewriting, infinitary λ-calculi, co-patterns<br><br>- Type systems: infinitary type systems, guarded recursive type theory<br><br>- Curry-Howard correspondence to linear temporal logic and functional<br>  reactive programming<br><br>- Semantics: denotational and interactive semantics for infinite data<br>  and computations<br><br>- Tools: extensions of programming languages and proof assistants to<br>  better treat infinite data, results on extending programming<br>  languages with primitives for manipulating infinite data such as<br>  streams in a more structured and convenient way, coinductive proof<br>  methods in proof assistants<br><br>- Proof theory and verification: the workshop will welcome works<br>  demonstrating how proof-theoretical investigations can be applied<br>  to model-checking problems, e.g. as in recent studies of higher-order<br>  recursive schemes or infinitary proofs.<br><br></div>