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 ESMTPS id 054B65D4 for ; Mon, 18 Jun 2018 09:58:59 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.51,238,1526335200"; d="scan'208";a="332228026" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 18 Jun 2018 11:58:56 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id D78C182491; Mon, 18 Jun 2018 11:58:56 +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 A657082474 for ; Mon, 18 Jun 2018 11:51:09 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dennis.mueller@fau.de; spf=Pass smtp.mailfrom=dennis.mueller@fau.de; spf=Pass smtp.helo=postmaster@mx-rz-1.rrze.uni-erlangen.de IronPort-PHdr: =?us-ascii?q?9a23=3AjD2FDRSauJ6YmTvfkjcUuuFS49psv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa6yZhKN2/xhgRfzUJnB7Loc0qyK6/2mATRIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSizexfbN/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf?= =?us-ascii?q?5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbD?= =?us-ascii?q?VwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlS?= =?us-ascii?q?gHLSY0/mHKhMJuj6xVrhyuqBNjzIDbe4yVKPlzc7nBcd8GS2dMXMBcXDFBDIOm?= =?us-ascii?q?aIsPCvIMM+hGoIn7oVsOrAC+ChGrCvvzzj9IgmH53bcn2OkmDA7JwgogH9QPsH?= =?us-ascii?q?TPttn1MboSXv6xzKnM0zrDdehb2Tnn54jVaBwuvO+DUKt2fMHMx0cvEAbFgU+R?= =?us-ascii?q?qYzjJz6ayP4Cs3Ob7uV8VeKgkW8nqxtrrjio3McshZHFhoEby1/e7yV23Jw5Jd?= =?us-ascii?q?y+SE51Zt6pFoZbuSKCN4ZuX88vTXxktDwnxrAFupO3ZjUGxIk9yxLBd/CLa5aE?= =?us-ascii?q?7g7/WOqMJDp1hXxodbG6ihmo7USs1vHwW8yp3FpWsCZIktzBu3UQ2xHc7MWMV+?= =?us-ascii?q?Fz8V272TmV0gDe8uFELl4wlarcM5Mhx7ExmoMJsUXCByP6hV/6jLWMdkQl5Oek?= =?us-ascii?q?8fnnYrPnppOFKYB0kAX+Pb4omsywH+s4NBICUHWF9uik1b3j+1P2QKlSg/ErnK?= =?us-ascii?q?TVrYrWKdkYq6O6GQNZz5sv5wyhAzu6yNgYmGMILFNBeBKJlYjpPFTOLejlAvih?= =?us-ascii?q?hVSsljZrx+vcMr3kH5XCMHzDkLP/crZn8ENcxhA8zc1F651JFL4NOOjzVVPptN?= =?us-ascii?q?zEEh85NBS5zPr9B9V40oMSQGaPAq6CMKPOqlKI/eIuI+yUZIAPojr9Kv4l5+Tv?= =?us-ascii?q?jXAjg1Mdc7OpjtMrbyWzF/FiZkGYembEg9EbEG5MsBBtYvbtjQiuXDhVZm2Fej?= =?us-ascii?q?Y44jwhQNaqAIHFR5vrhaGM2CO2BLVYb30ABl3aQiSgTJmNR/pZMHHaGcRmiDFR?= =?us-ascii?q?DeHwGb9k7gmnsUrB85QiK+PV/iMCspezhtZ8+qvfmENrrGAmP4Gmy2iIClpMsC?= =?us-ascii?q?YQXTZmjq52vApxxwXbiPUqs7ljDdVWoshxfEI6OJrblLQoDsC3QBCEJ5GTUkSr?= =?us-ascii?q?BMigAHQ8VNY4xdADZQBxFof7gw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CBAwD+fydbhxQLvINVBh4BBgyCdYE1f?= =?us-ascii?q?yiDeZRSgVaHOo9YCyOBVIVOGgYBBDQUAQIBAQEBAQEBAQETAQEBCgsJCCkjDII?= =?us-ascii?q?1IoJ1Bg8BBQgBASYDDzQCJgJsCAEBF4MKAoF/AQ6oMW2CHIJxAQEFgWODQiWBY?= =?us-ascii?q?AiBC4ZAgQmCE4EzhXsBAxiBOFuCNIJVh1mEZYN9iF0HAnhChEKJB4FFQYV2CgU?= =?us-ascii?q?khRKJI2+HO4FYgV0OCHFPgkMJggwahAGCJoI7hT0DbZBRAQE?= X-IPAS-Result: =?us-ascii?q?A0CBAwD+fydbhxQLvINVBh4BBgyCdYE1fyiDeZRSgVaHOo9?= =?us-ascii?q?YCyOBVIVOGgYBBDQUAQIBAQEBAQEBAQETAQEBCgsJCCkjDII1IoJ1Bg8BBQgBA?= =?us-ascii?q?SYDDzQCJgJsCAEBF4MKAoF/AQ6oMW2CHIJxAQEFgWODQiWBYAiBC4ZAgQmCE4E?= =?us-ascii?q?zhXsBAxiBOFuCNIJVh1mEZYN9iF0HAnhChEKJB4FFQYV2CgUkhRKJI2+HO4FYg?= =?us-ascii?q?V0OCHFPgkMJggwahAGCJoI7hT0DbZBRAQE?= X-IronPort-AV: E=Sophos;i="5.51,238,1526335200"; d="scan'208";a="332226155" Received: from mx-rz-1.rrze.uni-erlangen.de ([131.188.11.20]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 18 Jun 2018 11:51:08 +0200 Received: from mx-rz-1.rrze.uni-erlangen.de (mx-rz-1.rrze.uni-erlangen.de [IPv6:2001:638:a000:1025::14]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by mx-rz-1.rrze.uni-erlangen.de (Postfix) with ESMTPS id 418RDr0cRTz8vQP for ; Mon, 18 Jun 2018 11:51:08 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=fau.de; s=fau-2013; t=1529315468; bh=amLPqXj9y+Pc+58svYkSBXbnXL/gVgJBUC/qqhocqGQ=; h=From:Subject:To:Date:From:To:CC:Subject; b=IZrKi3dDoQLiHGnMnM6JMliuZUuISZSKefnkYTyM/GHQZUTiN2dmF3TNhNv4MkQJe HKdQsBmBVTXu4olW7OLREHhFeczP/G2LHH8vcSsBtEw27vnuUNaXWbZGKj9H/sUInr aJc72eX2crpBnXse7VG0hSRnKKsDEPc8lFpDWEWDraTxkql9S1cXV6hNZ/U8tFt+BP PQGpL/EPATTIooYbh+axc44JnLi1BBcnvYrEAFN+MueAdzDTquqTFJuz4dZZLT38Zz VPX/C5RmLzbCB8gme9Lx0ONAviN8yuMrdUrDtXzORtHmVU1/gTucAHYSABvThbZpll Qn9rJhYplb16A== X-Virus-Scanned: amavisd-new at boeck2.rrze.uni-erlangen.de (RRZE) X-RRZE-Flag: Not-Spam X-RRZE-Submit-IP: 10.188.48.143 Received: from [10.188.48.143] (kwarc23.informatik.uni-erlangen.de [10.188.48.143]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) (Authenticated sender: U2FsdGVkX18D1OGgrSfYl3X37K4vBGxzeX493UXRW/U=) by smtp-auth.uni-erlangen.de (Postfix) with ESMTPSA id 418RDn06K3z8vFq for ; Mon, 18 Jun 2018 11:51:05 +0200 (CEST) From: =?UTF-8?Q?Dennis_M=c3=bcller?= To: caml-list@inria.fr Message-ID: <63820f89-6f33-f8de-a24a-baed957b182e@fau.de> Date: Mon, 18 Jun 2018 11:51:04 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.8.0 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 8bit X-Validation-by: dennis.mueller@fau.de Subject: [Caml-list] Call for Opinions: FLoC Workshop on Modular Knowledge (Tetrapod18) Reply-To: =?UTF-8?Q?Dennis_M=c3=bcller?= X-Loop: caml-list@inria.fr X-Sequence: 16948 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: Workshop on Modular Knowledge, July 13. 2018 at FLoC http://kwarc.info/events/Tetrapod-2018/ ============================= Modularity has been recognized in all FLoC-related communities as an essential component of representation languages, computer-based tools, and knowledge exchange. The workshop will employ an unusual format: it will consist of six topical discussion-oriented sessions. These are introduced by a short thought-provoking invited talk on modularity in the speaker's respective field of expertise. Each block of three sessions is followed by additional time for discussions. Invited Speakers and Topics are: - Proof Checking (Catherine Dubois) - Large Proofs (Georges Gonthier) - Ontologies (Till Mossakowski) - Proof Assistants (Natarajan Shankar) - Software Synthesis (Doug Smith) - Mathematical Computation (Nicolas Thiery) To improve the discussions, we invite all interested researchers (independent of whether they attend the workshop) to submit preformulated opinions, either on one of the 6 subtopics or on modularity in general. Opinions include any valuable contribution to the discussion such as - position statements - strengths and weaknesses of existing solutions - pointers to pertinent recent or ongoing work - challenge and benchmark problems Opinions should be brief enough that workshop participants can easily read all opinions at the beginning of each session. Typically, they will not be longer than a couple of paragraphs. The organizers will curate the submitted opinions and publish them on the workshop website and in a post-workshop summary. For the version circulated at the workshop, the organizers may (with the collaboration of the authors) summarize or merge individual opinions if that helps readability. The online version will list all opinions verbatim. Opinions will be listed together with the name(s) of the authors. Submission via easychair: https://easychair.org/conferences/?conf=tetrapod18 -- Dennis M. Müller "To do mathematics is to be, at once, touched by fire and bound by reason. This is no contradiction. Logic forms a narrow channel through which intuition flows with vastly augmented force" - Jordan Ellenberg (How Not to Be Wrong) -- 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