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 D27AF5D5 for ; Fri, 6 Apr 2018 14:19:21 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.48,415,1517871600"; d="scan'208,217";a="321649218" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 06 Apr 2018 16:19:19 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id F3DEE82447; Fri, 6 Apr 2018 16:19:18 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id F142E8242A; Fri, 6 Apr 2018 15:59:19 +0200 (CEST) Authentication-Results: mail3-smtp-sop.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=3ArrywMBAUyS2miYQkXBqyUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSP36p82wAkXT6L1XgUPTWs2DsrQY07GQ6/iocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbAhEmDSwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+?= =?us-ascii?q?NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjD?= =?us-ascii?q?QhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlC?= =?us-ascii?q?YHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95RWSJPAY2y?= =?us-ascii?q?cpUBAPYaMOlCs4XwvUEDoQeiCQSuAu7k1z9GhmXx3a0/y+ksDQXG0xIvHtIPq3?= =?us-ascii?q?Tfscj7O70PUeCvzanIyyjIYfBK1zn+6IbDbxcsruuIXb1ufsvRyFIvGxnejlqK?= =?us-ascii?q?tIzlJTKV1uIWvmia9epgVOyvh3QpqwFruzWiwNonhIfOhoIQ0F/E9CN5zZ4rKt?= =?us-ascii?q?KiU056YcKrEJtKuCGbLYt6WMQiQ3tnuCoiy70Go5+7fCYQxJQp3R7SbeGMfYuQ?= =?us-ascii?q?4h/7SeqcJTh1iGh7dL+/iBu+60mtxvDmWsWp3ltHrTJJnsfQun0JzRDe6ciKRu?= =?us-ascii?q?Fj8ku82juDzQDe5+5CLEspj6TUMYQhzaQ1lpcLsUTMACv2mELuga+VcUUk4O+o?= =?us-ascii?q?6+D5bbX4vJOcKol0igDgMqg3gsywG/44MgkVX2WZ4+i82qfj8VX4QLVMkPI2jr?= =?us-ascii?q?HUvI3eKMkUvKK1HQ9Y34k55xu+EjuqyskUkHcEIV5dfRKIlYnpO1XAIPDiCve/?= =?us-ascii?q?hkyhny1vx//YMbzhA47NImLYkLj7YLZ98U9cyAwowNBe/ZJUC78BLOj9Wk/rrN?= =?us-ascii?q?DYFAM2MxSow+b7D9Vwzp8RVniKAq+dKa/StV6I5vkzI+SXf48UuDP9K+A/6PL0?= =?us-ascii?q?jH85n0Udfaiz0pcNZnC4BOxsI1+Fbnr0ntcBDWAKsxIiQ+ztkV2OSCJcZ3KvX6?= =?us-ascii?q?0n/Tw7E4KnDYLbRo+3mrCB3SG7HodXZm9cEFyMH23oJM24XKIQeTqfOYpolDoD?= =?us-ascii?q?SL6qRqcl1Aqyr0nhxrN8aPfM9yse85/vyZw96OHJ0BA33TN4FYGc1ieDVSU8hn?= =?us-ascii?q?kPQDEq3K14u11VzlaYzbM+ifVEFZpa7LVUUUNyf6346MNbIOW6fwvAetaPRx6C?= =?us-ascii?q?Q866S3llStU+wtQmZk9hG5O/iBGG1S2sBfkZmurPTLsf+6fYl134JsJ8zXmO8K?= =?us-ascii?q?g6kxFyScJKMSiih7Vj3wnVHY/A1UuDweLifqMFmSXJ6W2rzGyUvUgeXhQ0GaXM?= =?us-ascii?q?RnMSYk/+rd3i5U7GS/mpE7t0HBFGzJurLqZaa8ahtlxbXvblcPXkQkz5z260CA?= =?us-ascii?q?aJ3fWXZZfwemM13T/cBg4KiVZArj69KQEiC3L58CrlBzt0GAeqOhu0qLgsmDaA?= =?us-ascii?q?VkYxijqyQQhk3rux9AQSgK3OSukS0PQKonV48mkmLBOGx9vTTuG4iU95ZqwNM9?= =?us-ascii?q?In4VkB23iL71UgbKzlFLhrgxslSyoyv07q0E8rWIZHi88uoW1s0QxzN+eA2UlA?= =?us-ascii?q?bGze04qiYrA=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AfAgC2e8dah4o9/sJdDggIAQYMgm+BN?= =?us-ascii?q?G8yg1WBHYdBjCyCA2YagWUBAYwNhl4LI4RggjMHGQcBBDQUAQIBAQEBAQEBAQE?= =?us-ascii?q?TAQEBCgsJCCgjDII1JAGCZwUGRQwFGQ03AiEDEgEFASIBGoUFAQMLjTqPezyLB?= =?us-ascii?q?YIcFIgzgiWHa4FUP4EMglCDOgsEGIEfgyOCVAKLd4tMCBpVhGWCToYRgW2BZIh?= =?us-ascii?q?vgh6GfoZDAgQGBQIFDgEDHoECAjOBQQEbDggzQXwGgXwBEAiCJRqEcoNWhQQ5A?= =?us-ascii?q?48HAQE?= X-IPAS-Result: =?us-ascii?q?A0AfAgC2e8dah4o9/sJdDggIAQYMgm+BNG8yg1WBHYdBjCy?= =?us-ascii?q?CA2YagWUBAYwNhl4LI4RggjMHGQcBBDQUAQIBAQEBAQEBAQETAQEBCgsJCCgjD?= =?us-ascii?q?II1JAGCZwUGRQwFGQ03AiEDEgEFASIBGoUFAQMLjTqPezyLBYIcFIgzgiWHa4F?= =?us-ascii?q?UP4EMglCDOgsEGIEfgyOCVAKLd4tMCBpVhGWCToYRgW2BZIhvgh6GfoZDAgQGB?= =?us-ascii?q?QIFDgEDHoECAjOBQQEbDggzQXwGgXwBEAiCJRqEcoNWhQQ5A48HAQE?= X-IronPort-AV: E=Sophos;i="5.48,415,1517871600"; d="scan'208,217";a="261135937" Received: from korolev.univ-paris7.fr ([194.254.61.138]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 06 Apr 2018 15:59:18 +0200 Received: from potemkin.univ-paris7.fr (potemkin.univ-paris7.fr [IPv6:2001:660:3301:8000::1:1]) by korolev.univ-paris7.fr (8.14.4/8.14.4/relay1/75695) with ESMTP id w36DxI5F004321 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO); Fri, 6 Apr 2018 15:59:18 +0200 Received: from mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [81.194.30.253]) by potemkin.univ-paris7.fr (8.14.4/8.14.4/relay2/75695) with ESMTP id w36DxKL2025219; Fri, 6 Apr 2018 15:59:20 +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 85179EB5C9; Fri, 6 Apr 2018 15:59:18 +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 YOpcwSTOq6i0; Fri, 6 Apr 2018 15:59:16 +0200 (CEST) Received: from mail-oi0-f54.google.com (mail-oi0-f54.google.com [209.85.218.54]) (Authenticated sender: saurin) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTPSA id 9A2D3EB33C; Fri, 6 Apr 2018 15:59:16 +0200 (CEST) Received: by mail-oi0-f54.google.com with SMTP id q71-v6so1110242oic.6; Fri, 06 Apr 2018 06:59:16 -0700 (PDT) X-Gm-Message-State: ALQs6tCAxRp8gxv0qscetsnIT5992szCF4j6BIR5rdoFSkwyBlcFxmeh GlLDtZpb9AdjvNbeuGAjuRUIP54GwFLwIdJTxUQ= X-Google-Smtp-Source: AIpwx48TPhp92plZeZlGQxcWPtplIslLkhm9LOpMHdVObMO5nJqHB78zy0nZxxF81OjkH9bFiUe8d9WvGXGQzwEJrXs= X-Received: by 2002:aca:ef57:: with SMTP id n84-v6mr14555300oih.5.1523023155502; Fri, 06 Apr 2018 06:59:15 -0700 (PDT) MIME-Version: 1.0 Received: by 10.74.209.21 with HTTP; Fri, 6 Apr 2018 06:58:54 -0700 (PDT) From: Alexis Saurin IRIF Date: Fri, 6 Apr 2018 15:58:54 +0200 X-Gmail-Original-Message-ID: Message-ID: To: types-announce@lists.seas.upenn.edu, 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="0000000000002b24be05692e76e0" X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (korolev.univ-paris7.fr [IPv6:2001:660:3301:8000::1:2]); Fri, 06 Apr 2018 15:59:18 +0200 (CEST) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (potemkin.univ-paris7.fr [194.254.61.141]); Fri, 06 Apr 2018 15:59:20 +0200 (CEST) X-Miltered: at korolev with ID 5AC77D36.002 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-Miltered: at potemkin with ID 5AC77D38.003 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-j-chkmail-Enveloppe: 5AC77D36.002 from potemkin.univ-paris7.fr/potemkin.univ-paris7.fr/null/potemkin.univ-paris7.fr/ X-j-chkmail-Enveloppe: 5AC77D38.003 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 : 5AC77D36.002 on korolev.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Score: MSGID : 5AC77D38.003 on potemkin.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Status: Ham X-j-chkmail-Status: Ham X-Validation-by: alexis.saurin@irif.fr Subject: [Caml-list] PARIS workshop @ FLoC 2018 : Programming And Reasoning on Infinite Structures - CFP Reply-To: Alexis Saurin IRIF X-Loop: caml-list@inria.fr X-Sequence: 16780 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: --0000000000002b24be05692e76e0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable (apologies for multiple copies...) ** NEW ** - invited speakers announced - additional details on submission procedure =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: Submissions: April 15 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= --0000000000002b24be05692e76e0 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

(apologies for multiple copies...)

** NEW ** - invited speakers announced
- additional details on submission proce= dure

=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 Papers

=C2=A0=C2=A0 Programming And Reasoning on Infinite Struc= tures
=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, Ju= ly 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 form= al methods to program and reason about infinite data,
whether inductive = or coinductive, is challenging and subject to
numerous recent research e= fforts. The understanding of the logical
and computational principles un= derlying 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 proof= s, guarded recursive type theory, research effort on
integrated coinduct= ion in proof assistants, concrete semantics of
coinductive computation, = recent developments in infinitary rewriting,
or the unveiling of the Cur= ry-Howard correspondence between temporal
logics and functional reactive= programming, to name a few.

The workshop aims at gathering research= ers working on these topics
as well as colleagues interested in understa= nding the recent results
and open problems of this line of research:
=
- For outsiders, the workshop will offer tutorial sessions and
=C2= =A0 survey-like invited talks.
- For specialists of the topic, the works= hop will permit to gather
=C2=A0 people working with syntactical or sema= ntical methods, people
=C2=A0 focusing on proof systems or programming l= anguages, and foster
=C2=A0 exchanges and discussions benefiting from th= eir various
=C2=A0 perspectives.

We are seeking for short submiss= ions (~3-4 pages long, easychair
style) presenting
(i) new completed = results
(ii) work in progress, or
(iii) advertising recently publishe= d results.

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


** Important dates and submission details:

Su= bmissions: April 15
Notification: May 15
Final abstract: May 25
Wo= rkshop: July 7 and 8

Submission page: http://easychair.org/conferences/?conf=3Dpar= is18

Submission style: https://easychair.org/publications/for_authors
Website: https:= //www.irif.fr/~saurin/RAPIDO/PARIS-2018/


** Program Committe= e:

Andreas Abel =C2=A0 =C2=A0 (Gothenburg University)
David Baeld= e =C2=A0 =C2=A0 (ENS Paris-Saclay & Inria Paris; co-chair)
Amina Dou= mane =C2=A0 =C2=A0(CNRS and ENS Lyon)
Martin Lange =C2=A0 =C2=A0 (Univer= sity of Kassel)
Rasmus M=C3=B8gelberg (IT University of Copenhagen)
L= uke Ong =C2=A0 =C2=A0 =C2=A0 =C2=A0 (University of Oxford)
Andrew Polons= ky =C2=A0(Appalachian State University)
Colin Riba =C2=A0 =C2=A0 =C2=A0 = (ENS Lyon and CNRS)
Alexis Saurin =C2=A0 =C2=A0(CNRS and Paris Diderot U= niversity; co-chair)
Alex Simpson =C2=A0 =C2=A0 (University of Ljubljana= )


** Invited speakers:

Bahareh Afshari (University of Got= henburg)
James Brotherston (University College London)
Pierre Hyverna= t (Savoie Mont-Blanc University)

** Topics:

Suggested, but no= t exclusive, topics of interest for the workshop are:

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

- Calculi: infinitary r= ewriting, infinitary =C3=8E=C2=BB-calculi, co-patterns

- Type system= s: infinitary type systems, guarded recursive type theory

- Curry-Ho= ward correspondence to linear temporal logic and functional
=C2=A0 react= ive programming

- Semantics: denotational and interactive semantics = for infinite data
=C2=A0 and computations

- Tools: extensions of = programming languages and proof assistants to
=C2=A0 better treat infini= te data, results on extending programming
=C2=A0 languages with primitiv= es for manipulating infinite data such as
=C2=A0 streams in a more struc= tured and convenient way, coinductive proof
=C2=A0 methods in proof assi= stants

- Proof theory and verification: the workshop will welcome wo= rks
=C2=A0 demonstrating how proof-theoretical investigations can be app= lied
=C2=A0 to model-checking problems, e.g. as in recent studies of hig= her-order
=C2=A0 recursive schemes or infinitary proofs.
--0000000000002b24be05692e76e0--