From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 E22BE8239C; Fri, 2 Mar 2018 13:13:10 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=david.baelde@gmail.com; spf=Pass smtp.mailfrom=david.baelde@gmail.com; spf=None smtp.helo=postmaster@mail-wm0-f52.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of david.baelde@gmail.com) identity=pra; client-ip=74.125.82.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="david.baelde@gmail.com"; x-sender="david.baelde@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of david.baelde@gmail.com designates 74.125.82.52 as permitted sender) identity=mailfrom; client-ip=74.125.82.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="david.baelde@gmail.com"; x-sender="david.baelde@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wm0-f52.google.com) identity=helo; client-ip=74.125.82.52; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="david.baelde@gmail.com"; x-sender="postmaster@mail-wm0-f52.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AKwrPDx94tTk0Gf9uRHKM819IXTAuvvDOBiVQ1KB2?= =?us-ascii?q?0eocTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/?= =?us-ascii?q?8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1?= =?us-ascii?q?Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+?= =?us-ascii?q?RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTF?= =?us-ascii?q?UACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiC?= =?us-ascii?q?gZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsaS2RPXchfSjJPDZ+n?= =?us-ascii?q?YoQVE+YMJ/xVo5Xhq1YMqxa1GAmiBPnoyj9NnnL407c10/ogEQ7bwQctAsgBv2?= =?us-ascii?q?rQrNroKqgZTOe4w7TSwjXdbvNZxC3x55PSfR8/pfGDQKx/fNHeyUkqDQzFj1GQ?= =?us-ascii?q?pZb5MDOS0+QAqm6W5PduW+Kojm4osQBxoj63y8gykIbJnYIUxUzE9SpjwYY1P8?= =?us-ascii?q?e0SElhYd6rCJdQtjuaN4p4Qs84TWFooiA3waAFt56jZCUHypsqywTCZ/CZc4WE?= =?us-ascii?q?+BHuWPiLLTp4mn5ofq+0iQyo/ki60OL8U9G50FZUoSpBldnBrnUN2AbS6siDU/?= =?us-ascii?q?d88EKh1SqW2wDd6uxIP1o4laXcK54mzb4wkoQcvV7fES/xnUX6lK6WdkM69ei0?= =?us-ascii?q?8+nqYLrrqoWBO4NqigzyKKcjltKlDek4LAQCR22b9v691L3n8035WrJKjvgun6?= =?us-ascii?q?bEqp/aO8UbqbOjDwBOyIks9RK/ACq439kDknkHKUhKeBODj4TzJ17OJ/X4Ae+l?= =?us-ascii?q?g1uwiDdr2+zGPrr5D5rRNHfDlbPhca95605d0woz0ctS54lUC7EEOPL8QFX9tN?= =?us-ascii?q?3eDh8jMgy72fzrCNtn1okGQ2KAHreZML/OsV+P/u8gP+6MZJYMtDnhL/gl+uXh?= =?us-ascii?q?gGQimV4deKmpxYEYZGq5HvRgOUWZYGDjjs0PEWcQ7UICS7nNo1SHVXZ2bne2Xq?= =?us-ascii?q?QzrhU6E57uWYzKQ4TohL2awA+6GIdXbyZIEAbIWXzvbsCPX+oGQCOUOM5o1DIe?= =?us-ascii?q?EfChQpQi2BWqnA/z0LlqKu6S/TcX5rz5090gy+TNlB163zV5C8iQmzWBRn91ki?= =?us-ascii?q?UCTjIy0K1Xrkl0y1PF2q991a8LXedP7u9EB19pfaXXyPZ3XpWrAlqYL4W5DW2+?= =?us-ascii?q?S9DjOgkfC9c4wtsAeUF4QozwgRXK3i7sCLgQxeXSWM4Et5nE1n20HP5Tjm7c3f?= =?us-ascii?q?B43VYjS8pLc2ahg/wnrlWBN8vyi0yc0p2SW+Ec0SrKrjrRyGOPuARHVVY1X/if?= =?us-ascii?q?G38YYUTSoJLy4UaQF7I=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DHAgDPPplahjRSfUpdFgmCbIEdAT5wK?= =?us-ascii?q?AqDSoE2lmaCfRuID4Z+hSCCFQojh2kHGQcBBDEXAQIBAQEBAQEBAQESAQEBCAs?= =?us-ascii?q?LCCgugjgkAYJlCx0BGwwMBgMSEDcCJAERAQUBIgGFFAEDFRCcSECMFIIFBQEcF?= =?us-ascii?q?4JrBYNVChknDVdZgiMCBhKFFIIpgVeBZoJ3g1kLBBmEYYJiBI13jGcJggyERoM?= =?us-ascii?q?ShxmCNYITijCJfIdFFAUggQkfAYFWHA4IMxojgQCCAgEPCYFvSSKBZAI/N4xMA?= =?us-ascii?q?QEB?= X-IPAS-Result: =?us-ascii?q?A0DHAgDPPplahjRSfUpdFgmCbIEdAT5wKAqDSoE2lmaCfRu?= =?us-ascii?q?ID4Z+hSCCFQojh2kHGQcBBDEXAQIBAQEBAQEBAQESAQEBCAsLCCgugjgkAYJlC?= =?us-ascii?q?x0BGwwMBgMSEDcCJAERAQUBIgGFFAEDFRCcSECMFIIFBQEcF4JrBYNVChknDVd?= =?us-ascii?q?ZgiMCBhKFFIIpgVeBZoJ3g1kLBBmEYYJiBI13jGcJggyERoMShxmCNYITijCJf?= =?us-ascii?q?IdFFAUggQkfAYFWHA4IMxojgQCCAgEPCYFvSSKBZAI/N4xMAQEB?= X-IronPort-AV: E=Sophos;i="5.47,412,1515452400"; d="scan'208,217";a="316056328" Received: from mail-wm0-f52.google.com ([74.125.82.52]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 02 Mar 2018 13:13:09 +0100 Received: by mail-wm0-f52.google.com with SMTP id z81so2741181wmb.4; Fri, 02 Mar 2018 04:13:09 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=gAiShEl5y2luDncWC+avs8DYNdrnqXpZGO6g+Hk2EgE=; b=KwzCwU2LrYpIlM3OhFN7PKHQ0LL3ZrEc5WOZUplj7+hfXeSUAFa/B8B+WR8Z2/8HT4 nRw4xAlx0omAXT8kBzbhPYGrUxMR2kT1Q0ooAzNaa3gON8C/YocM72WT2oJ74iPiwvOW cThcVcAiBQsn3OehuVoRvHDiRvx4HjXJX+jGj/DGFZB1xnm05Z2RyfTzfw9jCh/tRGGU BuP3ssMsEQTkfUJ0hirmh9iphpZT9VjV3q21HWePp1Qg+ihE0vGwt9B1Kef1TFOSi+ax Z+kMa8QXtXtf5+Gyho0pr6xzRXLYe+jOlYXAVqj00J8ynewVQTCcGENgu8F0b9uC6e+o 0Osw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=gAiShEl5y2luDncWC+avs8DYNdrnqXpZGO6g+Hk2EgE=; b=eP5hk9t6DyNv8IOyxbtpzdzYBLxvUNElYktcwpAPf+yBEQeT8+fwKBMg2DFfQnxaVB ubQDJohPvA6O81d85pG8Byb7GfruiueZg/u90KP0AO8RdV+bIr2wQ/HyVTqHYLKm2Uy7 0QfRkHvyTfNOmNeLi+IVpVfIIvuzoo8hSIJ3BYotCoHsKvccaiTMGyzP6XC9RYFcaXE4 WIIRdMQQhWSv0k46M88avL10dXnTQ6alrwuSiQi+/Hax0HAlpaBpZdNFuKeTpGtBz/Ss FboBr9Lh7dWsegJPAAn/AA74J+NRN+cN1Ub27I/FeMBWMpUETykdFqI72KfSeaGvQa9Z snmg== X-Gm-Message-State: AElRT7EzivL4Iz5OOSaeO9aeg6JMREKXHm7s2gyuzKL787lvNfgYiozD YIQG6l7XKXa3U08+YxklAiN5mspWsBVjXzT1VTcJNTxD X-Google-Smtp-Source: AG47ELv6bKmZPxvW73G3V2Tc7jGPDlgXKFlyRkzCmaubjQiQsCwab0MKBtrzyo5GOo77xXAbFz4Lo5Gg4RWdwybWjVE= X-Received: by 10.28.14.6 with SMTP id 6mr1484460wmo.2.1519992789217; Fri, 02 Mar 2018 04:13:09 -0800 (PST) MIME-Version: 1.0 Received: by 10.28.132.80 with HTTP; Fri, 2 Mar 2018 04:12:48 -0800 (PST) From: David Baelde Date: Fri, 2 Mar 2018 13:12:48 +0100 Message-ID: To: OCaml Mailing List , coq-club@inria.fr, haskell@haskell.org Content-Type: multipart/alternative; boundary="001a114433be4335c905666ce6f4" Subject: [Caml-list] PARIS workshop @ FLoC 2018 : Programming And Reasoning on Infinite Structures (First CfP) --001a114433be4335c905666ce6f4 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Programming And Reasoning on Infinite Structures A workshop affiliated with FSCD@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=3Dparis18 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=C3=B8gelberg (IT University of Copenhagen) Luke Ong (University of Oxford) Andrew Polonsky (Appalachian State University) Colin Riba (LIP, ENS Lyon) Alexis Saurin (IRIF, Universit=C3=A9 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 =CE=BB-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. --001a114433be4335c905666ce6f4 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 
Programming And Reasoning on Infinite Stru=
ctures
A workshop affiliated with FSCD@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=3Dparis18

Website: https://www.irif.fr/~saurin/RAPIDO/PARIS-2=
018/


** 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=C3=B8gelberg (IT University of Copenhagen)
Luke Ong         (University of Oxford)
Andrew Polonsky  (Appalachian State University)
Colin Riba       (LIP, ENS Lyon)
Alexis Saurin    (IRIF, Universit=C3=A9 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 =CE=BB-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.
--001a114433be4335c905666ce6f4--