From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id 566435D5 for ; Mon, 16 Apr 2018 23:08:55 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.48,461,1517871600"; d="scan'208,217";a="323122498" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 17 Apr 2018 01:08:53 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id DEA8682443; Tue, 17 Apr 2018 01:08:52 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id D93158240C; Tue, 17 Apr 2018 00:41:55 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=alexis.saurin@irif.fr; spf=Pass smtp.mailfrom=alexis.saurin@irif.fr; spf=None smtp.helo=postmaster@korolev.univ-paris7.fr IronPort-PHdr: =?us-ascii?q?9a23=3A1nLUWRTUJFwz9ICXDrCW6IbDT9psv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa67ZReFt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRo?= =?us-ascii?q?LerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf?= =?us-ascii?q?5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXM?= =?us-ascii?q?TRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlD?= =?us-ascii?q?kIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZAo2y?= =?us-ascii?q?YYgBAfcfM+lEtITyvUcCoAGkCAWwGO/iyDlFjWL2060g1OQhFBnL0RAkH90Qv3?= =?us-ascii?q?XUrc71P7oPX++v0anI1zTDb/VL0jn+9IbGcRAvquyLUL1qdcre10YuFwLejlmK?= =?us-ascii?q?sozqJS6V1v4Ms2id9OdgVPivi28pqw1rrDiv3N4hh4/UjYwbzVDE8D92wIczJd?= =?us-ascii?q?CgVkF0e8WkEZtMuCGaLYR2Q9kiT3tvuCYgxb0KoZ+7fDILyJQp3RLfZeaHfo6V?= =?us-ascii?q?6RzgTOacOSp0iXZqdb6lmRq/8Uetxvf9W8WpylpGsyRIn9rUunwTyxDe7tKLR/?= =?us-ascii?q?h980u7xzqDygPe5vtELEwpk6fQNoQvzaQqlpUJtETOBi/2l1vyjK+Rbkgk+e+o?= =?us-ascii?q?6/7gYrXiuJCcKZV4ihz4MqQvhMyzGPw4PRIUX2ia4uSx1qfv/UPjQLlSj/02lL?= =?us-ascii?q?fWsIzCKMgGoqO0DBVZ3pgj5huwFTur0ckUkWMaIF9Lex+Ll43pNEvPIPD8A/e/?= =?us-ascii?q?mVOskDJzyv/cOr3uHJrMLnnYkLv7ZrZy8VNcyBAyzdBZ/J9UC6sBIPP9WkPrut?= =?us-ascii?q?zYFAc1MxaozOb/FNV9yoQeVHqTDa+eKaPeqEOH5uYyI+aXf4IVozb8K/095/H0?= =?us-ascii?q?l3M5mFkdfbOo3ZQNcny4EO5mKV2DYXXwmtcBDXsKvg0mQeP2klKCVDpTa2+2X6?= =?us-ascii?q?I9/TE7FJmrDZzDR4ComLyOxj23HpxQZmBcC1CDC23kd4ueW6REVCXHPt55nydB?= =?us-ascii?q?XL6nTJIn3hyGsA7h16EhNefd4WsFrZ/l0p546/CX3Ro18zdpFd6Q1WqcZ2V1hX?= =?us-ascii?q?8TSiUo0bo5vVFwjFGHleB3j+YdFNl76P9TFwY/c5DGi6RiEdf1VB7Bc9CTWX6i?= =?us-ascii?q?Q866Gnc7R84xhdYFJVt+X53ovTTk8AuBNvcwnr2PBZo7uobdxGS7b5J5zHnH34?= =?us-ascii?q?EkhkUmBNZJNCisgah5sQTeUcqBtG6QkqLiUK0d2C/L+y+nzHGS9BVTWQt0FKHE?= =?us-ascii?q?Rmw3Z03MrN2/6FmUC/elDq1iOQ9cw+aDLLFLY5vnlxEORP74O9naZ0qxknyzCB?= =?us-ascii?q?KMgLSWY9nEYWIYiQzZBVgFiEgo9GucNA52Jx2AjSqKBThjBVP0JVjl7PN/rlu6?= =?us-ascii?q?VE46iQ+QOR4yn4Gp8wIY0KTPA8gY2agJ7WJ4820tTQSNmunOAt/FnDJPOaBVYN?= =?us-ascii?q?cz+lBChDDYrQ1zeJK6ffk72gwuNj9vtkar7C1ZT51amJl4rWkrwkx8M/DAiQ4T?= =?us-ascii?q?R3ajxZn1f4bvBCzy8RSoMfKE2VbE19Kb5OES7vUm7k3qpgCySQws6Sc/3g=3D?= =?us-ascii?q?=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DKBAA9JdVabYo9/sJdDgiDXWEXYzKDX?= =?us-ascii?q?YEdh0OMNoIDZhqBZQEBjBeGZQsjhGCCPwcZBwEENBQBAgEBAQEBAQEBARMNCwk?= =?us-ascii?q?GKiMMgjUkAYJnBQZFDAUZDTcCIQMSAQUBIgGFHwQLikaPfzyLBYIcFIgtgiWIB?= =?us-ascii?q?oFUP4EPglaBdoFFCwQYgSODI4JUAowEi2AIGlaEaYJQhhKBMzuBZYE8hzyJLIZ?= =?us-ascii?q?kDwMegQICM4FBARsOCDNBK1IGgXwBEAiBZzyFDoNWhQQ5A48YAQE?= X-IPAS-Result: =?us-ascii?q?A0DKBAA9JdVabYo9/sJdDgiDXWEXYzKDXYEdh0OMNoIDZhq?= =?us-ascii?q?BZQEBjBeGZQsjhGCCPwcZBwEENBQBAgEBAQEBAQEBARMNCwkGKiMMgjUkAYJnB?= =?us-ascii?q?QZFDAUZDTcCIQMSAQUBIgGFHwQLikaPfzyLBYIcFIgtgiWIBoFUP4EPglaBdoF?= =?us-ascii?q?FCwQYgSODI4JUAowEi2AIGlaEaYJQhhKBMzuBZYE8hzyJLIZkDwMegQICM4FBA?= =?us-ascii?q?RsOCDNBK1IGgXwBEAiBZzyFDoNWhQQ5A48YAQE?= X-IronPort-AV: E=Sophos;i="5.48,460,1517871600"; d="scan'208,217";a="323121173" Received: from korolev.univ-paris7.fr ([194.254.61.138]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 17 Apr 2018 00:41:54 +0200 Received: from mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [81.194.30.253]) by korolev.univ-paris7.fr (8.14.4/8.14.4/relay1/75695) with ESMTP id w3GMfsPx029211; Tue, 17 Apr 2018 00:41:54 +0200 Received: from mailhub.math.univ-paris-diderot.fr (localhost [127.0.0.1]) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTP id 45757EB40A; Tue, 17 Apr 2018 00:41:54 +0200 (CEST) X-Virus-Scanned: amavisd-new at math.univ-paris-diderot.fr Received: from mailhub.math.univ-paris-diderot.fr ([127.0.0.1]) by mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [127.0.0.1]) (amavisd-new, port 10023) with ESMTP id IYqEVdKwXoEF; Tue, 17 Apr 2018 00:41:52 +0200 (CEST) Received: from mail-oi0-f51.google.com (mail-oi0-f51.google.com [209.85.218.51]) (Authenticated sender: saurin) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTPSA id 69CE9EB274; Tue, 17 Apr 2018 00:41:52 +0200 (CEST) Received: by mail-oi0-f51.google.com with SMTP id x9-v6so16166101oig.7; Mon, 16 Apr 2018 15:41:52 -0700 (PDT) X-Gm-Message-State: ALQs6tAq94d05unCnIst/2xm3s3WMBkhRcXUczPdEaWpren2QVeJM6os svnjiemGkHacSj8/OSC4u9I3AJvI62yS3xGBO20= X-Google-Smtp-Source: AIpwx4+HIKgIFVrn6vVOBBlPgcVTwl3c1o9FUBUHLDq57cVpqgpJVatTcoOtwHdH4iBVKB+Z7P3NZ68uF2PdoRL3NSg= X-Received: by 2002:aca:dec5:: with SMTP id v188-v6mr15179355oig.303.1523918511107; Mon, 16 Apr 2018 15:41:51 -0700 (PDT) MIME-Version: 1.0 Received: by 10.74.138.8 with HTTP; Mon, 16 Apr 2018 15:41:30 -0700 (PDT) From: Alexis Saurin IRIF Date: Tue, 17 Apr 2018 00:41:30 +0200 X-Gmail-Original-Message-ID: Message-ID: To: types-announce@lists.seas.upenn.edu, concurrency@listserver.tue.nl, gdr-im@gdr-im.fr, prooftheory@lists.bath.ac.uk, "[LOGIC] Mailing List" , OCaml Mailing List , coq-club@inria.fr, haskell@haskell.org Cc: David Baelde Content-Type: multipart/alternative; boundary="0000000000008574c40569feed78" X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (korolev.univ-paris7.fr [194.254.61.138]); Tue, 17 Apr 2018 00:41:54 +0200 (CEST) X-Miltered: at korolev with ID 5AD526B2.002 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-j-chkmail-Enveloppe: 5AD526B2.002 from mailhub.math.univ-paris-diderot.fr/mailhub.math.univ-paris-diderot.fr/null/mailhub.math.univ-paris-diderot.fr/ X-j-chkmail-Score: MSGID : 5AD526B2.002 on korolev.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Status: Ham X-Validation-by: alexis.saurin@irif.fr Subject: [Caml-list] PARIS 2018 (FLOC workshop): Deadline extended to *April 25* Reply-To: Alexis Saurin IRIF X-Loop: caml-list@inria.fr X-Sequence: 16825 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --0000000000008574c40569feed78 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable ** NEW ** - deadline extended to *April 25* - please register your submission title by *April 20* (details below) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D Call for Papers Programming And Reasoning on Infinite Structures PARIS Workshop Affiliated with FSCD@FLOC 2018 Oxford, UK, July 7&8, 2018 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D 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, easychair style) 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: Submission registration (NEW): April 20 Submissions (NEW): April 25 Notification: May 15 Final abstract: May 25 Workshop: July 7 and 8 Submission page: http://easychair.org/conferences/?conf=3Dparis18 Submission style: https://easychair.org/publications/for_authors Website: https://www.irif.fr/~saurin/RAPIDO/PARIS-2018/ ** Program Committee: Andreas Abel (Gothenburg University) David Baelde (ENS Paris-Saclay & Inria Paris; co-chair) Amina Doumane (CNRS and ENS Lyon) Martin Lange (University of Kassel) Rasmus M=C3=B8gelberg (IT University of Copenhagen) Luke Ong (University of Oxford) Andrew Polonsky (Appalachian State University) Colin Riba (ENS Lyon and CNRS) Alexis Saurin (CNRS and Paris Diderot University; co-chair) Alex Simpson (University of Ljubljana) ** Invited speakers: Bahareh Afshari (University of Gothenburg) James Brotherston (University College London) Pierre Hyvernat (Savoie Mont-Blanc University) ** 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 =C3=8E=C2=BB-calculi, co-patter= ns - 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. --=20 Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs= --0000000000008574c40569feed78 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
** NEW **
- deadline extended to *April 25*
- please r= egister your submission title by *April 20* (details below)

=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Call for Pap= ers

=C2=A0=C2=A0 Programming And Reasoning on Infinite Structures=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0 = PARIS Workshop
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 Affiliated with FSCD@FLOC 2018

=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0 Oxford, UK, July 7&8, 2018

=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=


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

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

The workshop= aims at gathering researchers working on these topics
as well as collea= gues interested in understanding the recent results
and open problems of= this line of research:

- For outsiders, the workshop will offer tut= orial sessions and
=C2=A0 survey-like invited talks.
- For specialist= s of the topic, the workshop will permit to gather
=C2=A0 people working= with syntactical or semantical methods, people
=C2=A0 focusing on proof= systems or programming languages, and foster
=C2=A0 exchanges and discu= ssions benefiting from their various
=C2=A0 perspectives.

We are = seeking for short submissions (~3-4 pages long, easychair
style) present= ing
(i) new completed results
(ii) work in progress, or
(iii) adve= rtising recently published results.

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


*= * Important dates and submission details:

Submission registration (N= EW): April 20
Submissions (NEW): April 25
Notification: May 15
Fin= al abstract: May 25
Workshop: July 7 and 8

Submission page: h= ttp://easychair.org/conferences/?conf=3Dparis18

Submission = style: https://easychair.org/publications/for_authors

Web= site: https://www.irif.fr/~saurin/RAPIDO/<= span class=3D"m_-4984309438437961038gmail-il">PARIS-2018/

** Program Committee:

Andreas Abel =C2=A0 =C2=A0 (Gothenburg Un= iversity)
David Baelde =C2=A0 =C2=A0 (ENS Paris-Saclay & Inria Paris; co-chair)
Amina Doumane =C2=A0 =C2=A0= (CNRS and ENS Lyon)
Martin Lange =C2=A0 =C2=A0 (University of Kassel)Rasmus M=C3=B8gelberg (IT University of Copenhagen)
Luke Ong =C2=A0 =C2= =A0 =C2=A0 =C2=A0 (University of Oxford)
Andrew Polonsky =C2=A0(Appalach= ian State University)
Colin Riba =C2=A0 =C2=A0 =C2=A0 (ENS Lyon and CNRS= )
Alexis Saurin =C2=A0 =C2=A0(CNRS and Paris Diderot University; co-chair)
Alex Simpson = =C2=A0 =C2=A0 (University of Ljubljana)


** Invited speakers:
=
Bahareh Afshari (University of Gothenburg)
James Brotherston (Univer= sity College London)
Pierre Hyvernat (Savoie Mont-Blanc University)
<= br>** Topics:

Suggested, but not exclusive, topics of interest for t= he workshop are:

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

- Calculi: infinitary rewriting, infinitary =C3=8E=C2=BB-cal= culi, co-patterns

- Type systems: infinitary type systems, guarded r= ecursive type theory

- Curry-Howard correspondence to linear tempora= l logic and functional
=C2=A0 reactive programming

- Semantics: d= enotational and interactive semantics for infinite data
=C2=A0 and compu= tations

- Tools: extensions of programming languages and proof assis= tants to
=C2=A0 better treat infinite data, results on extending program= ming
=C2=A0 languages with primitives for manipulating infinite data suc= h as
=C2=A0 streams in a more structured and convenient way, coinductive= proof
=C2=A0 methods in proof assistants

- Proof theory and veri= fication: the workshop will welcome works
=C2=A0 demonstrating how proof= -theoretical investigations can be applied
=C2=A0 to model-checking prob= lems, e.g. as in recent studies of higher-order
=C2=A0 recursive schemes= or infinitary proofs.
--0000000000008574c40569feed78--