[Agda] PARIS workshop @ FLoC 2018 : Programming And Reasoning on Infinite Structures (First CfP)

[Andreas Abel]

Programming And Reasoning on Infinite Structures
A workshop affiliated with FSCD at FLOC 2018
July 7&8, 2018
Oxford, UK


Developing formal methods to program and reason about infinite data,
whether inductive or coinductive, is challenging and subject to
numerous recent research efforts. The understanding of the logical
and computational principles underlying these notions is reaching
a mature stage as illustrated by the numerous advances that have
appeared in the recent years.

Various examples of this can be viewed in recent works on co-patterns,
infinite proof systems for logics with induction and coinduction,
circular proofs, guarded recursive type theory, research effort on
integrated coinduction in proof assistants, concrete semantics of
coinductive computation, recent developments in infinitary rewriting,
or the unveiling of the Curry-Howard correspondence between temporal
logics and functional reactive programming, to name a few.

The workshop aims at gathering researchers working on these topics
as well as colleagues interested in understanding the 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, and foster
   exchanges and discussions benefiting from their various
   perspectives.

We are seeking for short submissions (~3-4 pages long) presenting
(i) new completed results
(ii) work in progress, or
(iii) advertising recently published results.


The workshop is affiliated with FSCD 2018, as part of the
Federated Logic Conference of 2018 and is funded by French ANR,
RAPIDO project.


** Important dates and submission details:

Submissions: April 15
Notification: May 15
Final abstract: May 25
Workshop: July 7 and 8

Submission page: http://easychair.org/conferences/?conf=paris18

Website: https://www.irif.fr/~saurin/RAPIDO/PARIS-2018/


** Program Committee:

Andreas Abel     (Gothenburg University)
David Baelde     (LSV, ENS Paris-Saclay & Inria Paris; co-chair)
Amina Doumane    (LIP, ENS Lyon)
Martin Lange     (University of Kassel)
Rasmus Møgelberg (IT University of Copenhagen)
Luke Ong         (University of Oxford)
Andrew Polonsky  (Appalachian State University)
Colin Riba       (LIP, ENS Lyon)
Alexis Saurin    (IRIF, Université Paris Diderot; co-chair)
Alex Simpson     (University of Ljubljana)


** Invited speakers:

A tutorial and two invited talks will be announced shortly.


** Topics:

Suggested, but not exclusive, topics of interest for the workshop are:

- Proof systems: proof system for logics with least and greatest fixed
   points, infinitary and cyclic/circular proof systems

- Calculi: infinitary rewriting, infinitary λ-calculi, co-patterns

- 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 treat 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 verification: the workshop will welcome works
   demonstrating how proof-theoretical investigations can be applied
   to model-checking problems, e.g. as in recent studies of higher-order
   recursive schemes or infinitary proofs.


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/