From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 566E78239C; Thu, 1 Mar 2018 18:07:46 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=shankar@csl.sri.com; spf=None smtp.mailfrom=shankar@csl.sri.com; spf=None smtp.helo=postmaster@brightmail-internal3.sri.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of shankar@csl.sri.com) identity=pra; client-ip=128.18.89.25; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="shankar@csl.sri.com"; x-sender="shankar@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of shankar@csl.sri.com) identity=mailfrom; client-ip=128.18.89.25; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="shankar@csl.sri.com"; x-sender="shankar@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@brightmail-internal3.sri.com) identity=helo; client-ip=128.18.89.25; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="shankar@csl.sri.com"; x-sender="postmaster@brightmail-internal3.sri.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Af3mEhBCFvcUvOOB1B6pGUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPT8psbcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfO?= =?us-ascii?q?pWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnM?= =?us-ascii?q?VhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs7Ximi76F2Rx/pky?= =?us-ascii?q?cIKzo58GbMisNuka1QvRatqhNjz4LRZoyeKfhwcb7Hfd4CRmRPUMZfWCJODY2h?= =?us-ascii?q?c4QBAPEMPfpboobnu1cCsRWzCAuqCejyyjFInHj23agi3uo5Cw7GwBYvH8gUv3?= =?us-ascii?q?TWttr1MroZX/21zKbSyzXDbOlZ2S3g44XPaRAhoeuDXbRzccXL00kiDB/Kjk6U?= =?us-ascii?q?qYD/JDOVzOUNv3KH4OpnUOKikmgqoBx/rDiow8cjkIjJhoQNx1Df7yV5wZw5Ks?= =?us-ascii?q?G/SE5+Z9OvDZhetzmCOodrXM8vQHtktDs5x7EcupO2eDIGxIonyhLHdfCKfJKE?= =?us-ascii?q?7xP5WOqMIzp0mmhpdK+/ihuw90Wr1/fyWdOu0FlQqypIitnMuW4J1xzU8sWIUe?= =?us-ascii?q?F9/kau2TaPywDT7/tLIUEwlabCKp4hxKIwmYQJsUTFBCD2nEv7gLWNdkU+++ik?= =?us-ascii?q?8fjoYrLjppOENo90jB/xMrg2l8CiH+g1MRICU3WY9Oim17Du+Vf1TKtKg/Eul6?= =?us-ascii?q?nWqpHaJcAVpq6jBA9V154u6w2/Dzi81tQYnmMILEhedR2blIjpP0vCIOviDfe+?= =?us-ascii?q?mVijjDBrx/XeMr37HprNNmTDkKvmfbtl90FczxMzwclD6JJQF7EOO+n+WlTxtd?= =?us-ascii?q?zdFh82KRa4w+fhCNVn14MRQ3iDAqGDMKnKq1+H+vovI/WQZI8SoDvyN+Iq5/vq?= =?us-ascii?q?jXMgnV8dfLKp3YcMZXCjHvVmJl2ZbmD2jtcAF2cKpAs+Q/bwhF2MSz4AL0q1Cr?= =?us-ascii?q?866jAgA4ahForPA5qgi72Z3Sq9AoYENTNoEFeJRFHha4yeUvUFbmqpIsZnkTUe?= =?us-ascii?q?Hey6S4Yn1hi0nAThz/x8NOuS8Sod48GwnONp7vHewElhvQd/CN6Qhj3VFjAmri?= =?us-ascii?q?YzXzYzmZtHjwl4w1aH37J/hqUDR9dI47VSSAZ8PpnZnbQjV4LCHznZd9LMc26I?= =?us-ascii?q?B828CGhqHNkqx5kVeUc7ENKn3EiagniaRoQNnrnOP6Qat6LR23+qf5R30XfJ1L?= =?us-ascii?q?UkhlgiB8pJKWC8gKd7rE7IHY+PmEKcxf6n?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CoHQB5MphaexlZEoBdHQEBBQELAYQ2c?= =?us-ascii?q?CiDVIsXjF8fgxiRKYMDghUKH4FghhEZBgYyFgECAQEBAQEBAQEBEgEBCwsKByg?= =?us-ascii?q?uAYI4DIJXMg8BPgc2AgUWCwILAwIBAgE3GgEGCAEBWYQ+qw+CJ4Rzg3WCIiaBD?= =?us-ascii?q?4QXgXwrhTRARIF5gzODNBOCTwWOaYtvCYZSixqOBIZpgxJ8hi8CBAsCGQGBLiU?= =?us-ascii?q?DgU4BGgEOCDMaCBsVgVcIgR8IgkYmgWQiV4o2gkgBAQE?= X-IPAS-Result: =?us-ascii?q?A0CoHQB5MphaexlZEoBdHQEBBQELAYQ2cCiDVIsXjF8fgxi?= =?us-ascii?q?RKYMDghUKH4FghhEZBgYyFgECAQEBAQEBAQEBEgEBCwsKByguAYI4DIJXMg8BP?= =?us-ascii?q?gc2AgUWCwILAwIBAgE3GgEGCAEBWYQ+qw+CJ4Rzg3WCIiaBD4QXgXwrhTRARIF?= =?us-ascii?q?5gzODNBOCTwWOaYtvCYZSixqOBIZpgxJ8hi8CBAsCGQGBLiUDgU4BGgEOCDMaC?= =?us-ascii?q?BsVgVcIgR8IgkYmgWQiV4o2gkgBAQE?= X-IronPort-AV: E=Sophos;i="5.47,408,1515452400"; d="scan'208";a="256616074" Received: from brightmail-internal3.sri.com ([128.18.89.25]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 01 Mar 2018 18:07:44 +0100 X-AuditID: 80125919-623ff7000000659c-d5-5a98335bb152 Received: from mx3.csl.sri.com (mx3.csl.sri.com [130.107.1.31]) (using TLS with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by brightmail-internal3.sri.com (mailgate-internal.sri.com) with SMTP id 21.99.26012.B53389A5; Thu, 1 Mar 2018 09:07:39 -0800 (PST) Received: from Ns-MacBook-Air.local (c-24-6-172-157.hsd1.ca.comcast.net [24.6.172.157]) (authenticated bits=0) by mx3.csl.sri.com (8.14.4/8.14.4/Debian-2ubuntu2.1) with ESMTP id w21H7bFo026559 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES128-SHA bits=128 verify=NOT); Thu, 1 Mar 2018 09:07:38 -0800 Message-ID: <5A9832E8.3020003@csl.sri.com> Date: Thu, 01 Mar 2018 09:05:44 -0800 From: Natarajan Shankar User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:31.0) Gecko/20100101 Thunderbird/31.5.0 MIME-Version: 1.0 To: undisclosed-recipients:; Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Brightmail-Tracker: H4sIAAAAAAAAA02Se0xTZxjG853vOz3Hhs5j1Xm8REyXZYkGnMjIO6OE7A/3eUlc/McJWbTK iTRyMS3DS6JiYZlSxIOSCq1MVARGMWhLBZRSre1Wbxiuq1OEVHReuGiRxTila2NM+OfNL+/z PMn7Jg+P1e/YebwuO1fSZ2szNQolMe5EsXFpy8tTv276NR7q7aMs9NoaETQ8K0QQcoxy8LD5 HQf9FicL/wWuR3YtFwmcNV9lofbycQY6C44x4LhejWCsehGM+G0sVDmvIRgJyhjuXd0K7rph BN2tR1l4ZW9noVHeBgO2bgK97gEML06Oc2Dp6GcgWHqPg9DAGQSDgx8ITFSI4HKVsmDtiZzw pu0ugdfXhjFMvD+HoaKhAMHpYR8HtjcBBsJeN4JA+D6BPpuPhSvhDgY8oWICH25FfggcCRL4 OxxkoObUCIHAgw1gazFyUPe2lwU5dEsBN2sbCLzotEbGYRcC/2ClAjy2OxxUd3Qq4LjXwcFQ qwNDWZkRQ2/5GQz+u+0ITB4KjeeNLPzzyMampFO30cTR7p519LA/l1Y+7iL0kKkP064T+Yg6 f/mTUL/djuiYy4PofTmZtlrX0sL6o5iO1pcQWuVdT8PeUkTrrE7uh02pypXpUqYuT9IvTd6q zDhv8nC7xufscZc9RfmoZ2YR4nlRSBRPPs0rQtN4tdDEiG03EouQMsINjOgc6sNRQSUsFqv+ 6ldEmQhfip0XXpJoViHEic8mf4quZwvp4rjplOKjfYZ4s2KIRHmWsECstD5mozxTSBP/HTvE RRkLX4nvf+vCHzlWLHBasYxiLFPilik2yxRbFcL1aME2vW5HRm6WVpcZ96mHy+MNel389pws O4o0Ml+9eW4LKqlZ5UECjzQxKiGmPFXNavMMe7M8SOSxZpbqdrM5Va1K1+7dJ+lztuh/zpQM HjSfJ5o5qidy8Wa1sEObK+2UpF2S/pPK8NPm5SOXdq1ikSZlonZSLkqYveLsk++mt352MDsp KWV/me/A9uDCxLerY1bHutyXwrcTktZ87z0hryJp2bKl+Ithf0poWcaVxLk57ebYO7ubwmtq 2LaSb4Q/2nzKS0uWmhu/rdi42+zbYPpcSn44Y8mPCc8dzc9/vzzpYlVNhaKuBB+znKvWEEOG dtlirDdo/weWw3mnjQMAAA== X-Validation-by: shankar@csl.sri.com Subject: [Caml-list] Eighth Summer School on Formal Techniques, Atherton, California, May 19-25, 2018 Eighth Summer School on Formal Techniques, May 19 - May 25, 2018 Menlo College Atherton, California http://fm.csl.sri.com/SSFT18 Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the sixth in the series, will focus on the principles and practice of formal techniques, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in studying and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school can expect to have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions. The lecturers at the school include: * Emina Torlak (University of Washington) Solver-Aided Programming * Mooly Sagiv (Tel Aviv University) Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems * Nikhil Swamy and Jonathan Protzenko (Microsoft Research) Programming and Proving in F* and Low* * Andreas Abel (Chalmers/Gothenburg University) Introduction to Dependent Types and Agda * Dirk Beyer (Ludwig Maximilian University, Munich, Germany) Software Model Checking The main lectures in the summer school will be preceded by a two-day background course on logic: * Natarajan Shankar (SRI CSL) and Stephane Graham-Lengrand (Ecole Polytechnique) Speaking Logic We will also have invited talks by * Nina Narodytska (VMWare Research) Verifying Properties of Binarized Deep Neural Networks * Gordon Plotkin (U. Edinburgh, UK) Some Principles of Differentiable Programming Languages Research Papers * Edward A. Lee (UC Berkeley) Plato and the Nerd - The Creative Partnership of Humans and Technology Information about previous Summer Schools on Formal Techniques can be found at http://fm.csl.sri.com/SSFT11 http://fm.csl.sri.com/SSFT12 http://fm.csl.sri.com/SSFT13 http://fm.csl.sri.com/SSFT14 http://fm.csl.sri.com/SSFT15 http://fm.csl.sri.com/SSFT16 http://fm.csl.sri.com/SSFT17 We expect to provide support for the travel and accommodation for a limited number of students registered at US universities, but welcome applications from non-US students as well as non-students (if space permits). Non-US students will have to cover their own travel and will be charged around US$800 for meals and lodging. Applications should be submitted at the website http://fm.csl.sri.com/SSFT18 Applicants are urged to submit their applications before April 30, 2018, since there are only a limited number of spaces available. Non-US applicants requiring US visas are requested to apply early. We strongly encourage the participation of women and under-represented minorities in the summer school.