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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id A3516800F4 for ; Tue, 7 Mar 2017 21:00:57 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fm-announcements-bounces@lists.nasa.gov; spf=Pass smtp.mailfrom=fm-announcements-bounces@lists.nasa.gov; spf=Pass smtp.helo=postmaster@lists.nasa.gov Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of fm-announcements-bounces@lists.nasa.gov) identity=pra; client-ip=128.156.249.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="fm-announcements-bounces@lists.nasa.gov"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of fm-announcements-bounces@lists.nasa.gov designates 128.156.249.229 as permitted sender) identity=mailfrom; client-ip=128.156.249.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="fm-announcements-bounces@lists.nasa.gov"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@lists.nasa.gov designates 128.156.249.229 as permitted sender) identity=helo; client-ip=128.156.249.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="postmaster@lists.nasa.gov"; x-conformance=sidf_compatible; x-record-type="v=spf1" IronPort-PHdr: =?us-ascii?q?9a23=3AyyEQrR3UzcBC8Jk5smDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?sesVK//xwZ3uMQTl6Ol3ixeRBMOAuq8C17Cd6vu7EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQtFiT69bL9oIxi6swrdutQYjIZsN6081gbHrnxUdu?= =?us-ascii?q?pM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTY?= =?us-ascii?q?QguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhy?= =?us-ascii?q?kdNz497WrZlMp+gqxGqx6lvhBywovYbYeIP/R8Y6zdZ8sXS2pfUMZNWSJPAY2z?= =?us-ascii?q?b4oAAOQcJeZVrYvzq0YAoBeiGQaiC/3gyiRTi3/q36A61vgtHR3c0QA+Gd8FrX?= =?us-ascii?q?TarM/yNKcXSe25wq7GzSjFb/NR2Dbx8JXDfw4/rvGXR71wa9faxU0pGQ7Zklud?= =?us-ascii?q?t5XpMT2b2+gTr2SX6uRsXv+ohmE7tQ5xuSKgxt02hobTnI4Vz03E9SN+wIc0Pt?= =?us-ascii?q?C4TlR0YcW+H5dKuCGaMJV2T9okTmp1tig6zbgGtoS6fCgM0Jkn2hjfZOedf4eT?= =?us-ascii?q?+BLvTPieLi1jhHNlZL2/hwy98Um6yuHmUcm0yllKoyxYmdfPrnAAzwHf5taER/?= =?us-ascii?q?dn40us2TeC2xrN5uxLJU04j7TXJ4Alz7Ioi5YevkXOEjXrlEj3jKKabEYp9+ay?= =?us-ascii?q?5+j6YbjrooeQO5J1hwz6KKgihMyyDOsiPgQTRWSX5Oqx2KDl8EbkWrtFlOc2nb?= =?us-ascii?q?PcsJ3CJcQUuKq5AwhN34Yn6ha/FCum0M8CkXkBNl1FYwiIg5LmO1HJPvD0Ffa/?= =?us-ascii?q?g1Kynzd33/3KI6PtD5bXInTekLrsfKxx51BTxQc319xT+YxYB7UZLPL2QEDxtd?= =?us-ascii?q?jYDhEjMwyzxubqENt91oYHVW2VBK+ZNqTSsUKO5u0zPeaMYZEauDDhK/g+/vLh?= =?us-ascii?q?lng5mUIbfaa1w5QXc2u1HvBnI0WCfXrsmc0NEWEQsQolVuPmklKCUTlNZ3qqRa?= =?us-ascii?q?Iz+ik7CJ66DYfEXo2inKaO3CK/HpFPYmBGC0uMEWvzeoWfW/YMbTqSLdV7njwF?= =?us-ascii?q?U7ihUY4h2gu0uA/00bptNvDU9TEAtZL/yNh14PXelR8q9TxzE8Sdz2CNQH9unm?= =?us-ascii?q?4TRj423aV/rldnyliZy6R4gvpYFcZS5/xTSAs6O4TcxfRgC9/uQgLBYsuJSFG+?= =?us-ascii?q?T9WmHDE+UM4xzsQPYkZ8HtWtlQrD0DCwD78UkbyLHp00/bjG03j/PcZ302zG27?= =?us-ascii?q?U5j1k6XstPMnWrhq5h+AjJHIHGjUGZl6esdakH3S/N9WKDwnGUvE5CSgJwUKPF?= =?us-ascii?q?XWoeZkTMt9j56FnCHPeTD686OF5B1dKaMfkNLdnolkldAvHqI92YbGWv3GK5BB?= =?us-ascii?q?KNz7XLa5L2emIbx2LTDQ0NlQYU4HCNOA0zADu68F/YFyFkQFfmYkfw9rtwrTay?= =?us-ascii?q?SEkz0geBYkhs0aauvwQYnOGRUO872rMfpDxnrTxvFRCy2MyBEMeKpQdqYPBBZ8?= =?us-ascii?q?gg6kxMz2PTul9BOcnqIaUnj1gYdBlxtE7r2hNrEa1EkNM2tzUsxRF7b62fzhkJ?= =?us-ascii?q?Iz2dmJn2PLrKLGL/+R2pd7X+3lDFzM3Q/K4U4bI3rEu17y+zEU93uVB61d5Hlz?= =?us-ascii?q?O3647DFkJSdbvLeQMbrEIi5vuSNiIw/IrOk3QqNLSytS3q3dsyDa0qzQj2LIQX?= =?us-ascii?q?C7+NCAKnS55SPMOpMuF/3gak?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CPAAAoEL9YmOX5nIBdGwEBAQMBAQEJA?= =?us-ascii?q?QEBFQEBAQECAQEBAQgBAQEBhAdVBDEHjleQOJgCC4JChV9CFQEBAQEBAQEBAQE?= =?us-ascii?q?BEgEBAQEBCAsLBigkC4IzBAIDGQWCPQYBARodBgEBBAgCFgIGDAIDAQIGAgEBP?= =?us-ascii?q?gQECAMBGwkJAScEEwURBwSJXgUJr1GDDoMIAQEFh2cBAQEBAQUBAQEBAQEBAQE?= =?us-ascii?q?BARUIiFMIhB4BgVqBDwoEAwGDUIIxAYkLhlyMTAEBG4ZahhSFLYF7U4RPhhWDb?= =?us-ascii?q?ZM5N4EdCBkLOE4RAYQzHIFzdYdWDxcwWgGBDAEBAQ?= X-IPAS-Result: =?us-ascii?q?A0CPAAAoEL9YmOX5nIBdGwEBAQMBAQEJAQEBFQEBAQECAQE?= =?us-ascii?q?BAQgBAQEBhAdVBDEHjleQOJgCC4JChV9CFQEBAQEBAQEBAQEBEgEBAQEBCAsLB?= =?us-ascii?q?igkC4IzBAIDGQWCPQYBARodBgEBBAgCFgIGDAIDAQIGAgEBPgQECAMBGwkJASc?= =?us-ascii?q?EEwURBwSJXgUJr1GDDoMIAQEFh2cBAQEBAQUBAQEBAQEBAQEBARUIiFMIhB4Bg?= =?us-ascii?q?VqBDwoEAwGDUIIxAYkLhlyMTAEBG4ZahhSFLYF7U4RPhhWDbZM5N4EdCBkLOE4?= =?us-ascii?q?RAYQzHIFzdYdWDxcwWgGBDAEBAQ?= X-IronPort-AV: E=Sophos;i="5.36,258,1486422000"; d="scan'208";a="215932171" Received: from lists.nasa.gov ([128.156.249.229]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 07 Mar 2017 21:00:55 +0100 Received: from localhost (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id 4735C602E78; Tue, 7 Mar 2017 14:59:06 -0500 (EST) Received: from lists.nasa.gov ([127.0.0.1]) by localhost (lists.nasa.gov [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id whHcVO2bT4jD; Tue, 7 Mar 2017 14:59:06 -0500 (EST) Received: from LISTS.nasa.gov (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id F29CC6024E1; Tue, 7 Mar 2017 14:59:03 -0500 (EST) X-Original-To: fm-announcements@lists.nasa.gov Delivered-To: fm-announcements@lists.nasa.gov Received: from localhost (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id 1DD556021A4 for ; Tue, 7 Mar 2017 14:59:02 -0500 (EST) Received: from lists.nasa.gov ([127.0.0.1]) by localhost (lists.nasa.gov [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id kuskLAsPwSKB for ; Tue, 7 Mar 2017 14:59:02 -0500 (EST) Received: from ndmsvnpf102.ndc.nasa.gov (NDMSVNPF102.ndc.nasa.gov [198.117.0.152]) by lists.nasa.gov (Postfix) with ESMTPS id EE6BA601305 for ; Tue, 7 Mar 2017 14:59:01 -0500 (EST) X-Comment: SPF check N/A for local connections - client-ip=198.117.1.197; helo=ndjsppt103.ndc.nasa.gov; envelope-from=cesar.a.munoz@nasa.gov; receiver=fm-announcements@lists.nasa.gov DKIM-Filter: OpenDKIM Filter v2.11.0 ndmsvnpf102.ndc.nasa.gov 61F51401CDF6 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=nasa.gov; s=letsgomars; t=1488916741; bh=oz49Ap0sNQ0gDojIvgP192s0dqEg+GlpxaFyj4N2hwU=; h=From:To:Subject:Date:From; b=aUGfiLwCT6UYx9X+6WkH33uER3Vu3Hafd1dkMy7cxIkEyE7iaLM/2t6ov2DlcwHbR cfg1selL9dBezGiIeZs4EZ9d7F49XhRPcs7ClCRjKUjMWZKZGLFM5tcrLm2oDi/zws 8GErEMfWsGdTz8QUywuesjjEJ1mbbO/dSlJ0H2plG5CjCrclNS73WY8kGGT4BFWTnm K7R7T9l+y/0piW33eSYk9Gi+sQSCxEV3gA440rkQKfFLCk5XzESU2AFMqjODkSEiiq TV/ME1nCF9wPddxqR/y3Ds4GxhKRJAqHl/mvfndm6KCPOpxkZNg3HerqyLOkXmwnEp /pKJi0TGL1Fjw== Received: from ndjsppt103.ndc.nasa.gov (ndjsppt103.ndc.nasa.gov [198.117.1.197]) by ndmsvnpf102.ndc.nasa.gov (Postfix) with ESMTP id 61F51401CDF6 for ; Tue, 7 Mar 2017 13:59:01 -0600 (CST) Received: from pps.filterd (ndjsppt103.ndc.nasa.gov [127.0.0.1]) by ndjsppt103.ndc.nasa.gov (8.16.0.20/8.16.0.20) with SMTP id v27JucWc001495 for ; Tue, 7 Mar 2017 13:59:01 -0600 Received: from ndjscht108.ndc.nasa.gov (ndjscht108-pub.ndc.nasa.gov [198.117.1.208]) by ndjsppt103.ndc.nasa.gov with ESMTP id 29204trn1b-6 for ; Tue, 07 Mar 2017 13:59:00 -0600 Received: from NDJSMBX204.ndc.nasa.gov ([169.254.1.131]) by NDJSCHT108.ndc.nasa.gov ([198.117.1.178]) with mapi id 14.03.0319.002; Tue, 7 Mar 2017 13:56:48 -0600 From: "Munoz, Cesar (LARC-D320)" To: "fm-announcements@lists.nasa.gov" Thread-Topic: ITP 2017 - Final Call for Papers Thread-Index: AQHSl3z0dCiX12VkYUSCFvKkZS5mmw== Date: Tue, 7 Mar 2017 19:56:48 +0000 Message-ID: <44FBC8A0-9F3A-4151-B7A5-861BB7B77484@nasa.gov> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/f.1d.0.161209 x-originating-ip: [146.165.83.189] Content-ID: <5ABE0077D98F4C4AB40AA84CF3549720@mail.nasa.gov> MIME-Version: 1.0 X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:, , definitions=2017-03-07_15:, , signatures=0 X-Proofpoint-Spam-Details: rule=notspam policy=default score=0 spamscore=0 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1702020001 definitions=main-1703070156 X-Proofpoint-Envelope-Sender: cesar.a.munoz@nasa.gov X-BeenThere: fm-announcements@lists.nasa.gov X-Mailman-Version: 2.1.14 List-Id: NASA Formal Methods Announcements List-Unsubscribe: , List-Post: List-Help: List-Subscribe: , Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Errors-To: fm-announcements-bounces@lists.nasa.gov Sender: fm-announcements-bounces@lists.nasa.gov X-Validation-by: cesar.a.munoz@nasa.gov Subject: [Caml-list] [fm-announcements] ITP 2017 - Final Call for Papers *** Apologies for multiple copies, please redistribute *** FINAL CALL FOR PAPERS ITP 2017 8th International Conference on Interactive Theorem Proving Brasilia, Brazil September 26-29, 2017 http://itp2017.cic.unb.br SUBMISSION DEADLINES * April 3, 2017 (abstracts) * April 10, 2017 (full papers) GENERAL INFORMATION The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009. The eighth ITP conference, ITP 2017, will be held at Universidade de Brasilia, September 26-29, 2017. SCOPE OF CONFERENCE ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include but are not limited to the following: * formal aspects of hardware and software * formalizations of mathematics * improvements in theorem prover technology * user interfaces for interactive theorem provers * formalizations of computational models * verification of security algorithms * use of theorem provers in education * industrial applications of interactive theorem provers * concise and elegant worked examples of formalizations (proof pearls) PUBLICATION DETAILS The proceedings of the symposium will be published in the Springer's LNCS series. ** After the conference the authors of selected papers will be invited to submit revised papers for a special issue of the Journal of Automated Reasoning. ** PAPER SUBMISSIONS All submissions must be original, unpublished, and not submitted concurrently for publication elsewhere. Furthermore, when appropriate, submissions are expected to be accompanied by verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used. Submissions should be no more than 16 pages in length and are to be submitted in PDF via EasyChair at the following address: https://easychair.org/conferences/?conf=itp2017 Submissions must conform to the LNCS style in LaTeX. Authors of accepted papers are expected to present their paper at the conference and will be required to a sign copyright release form. In addition to regular papers, described above, there will be a rough diamond section. Rough diamond submissions are limited to 6 pages and may consist of an extended abstract. They will be refereed and be expected to present innovative and promising ideas, possibly in an early form and without supporting evidence. Accepted diamonds will be published in the main proceedings and will be presented as short talks. IMPORTANT DATES Abstract submission deadline: April 3, 2017 Full paper submission deadline: April 10, 2017 Author notification: June 2, 2017 Camera-ready papers: June 30, 2017 Workshops & Tutorials: September 23-25, 2017 Conference: September 26-29, 2017 INVITED SPEAKERS Moa Johansson, Chalmers University of Technology, Sweden Leonardo de Moura, Microsoft Research Cezary Kaliszyk, Universitaet Innsbruck, Austria (joint with TABLEAUX and FroCos) Katalin Bimbo, University of Alberta, Canada (joint with TABLEAUX and FroCos) Jasmin Blanchette, Inria and LORIA, Nancy, France (joint with TABLEAUX and FroCos) WORKSHOPS AND TUTORIALS There will be a three-day programme of four workshops and four tutorials from 23-25 September. Workshops: 12th Logical and Semantic Frameworks with Applications (LSFA 2017) Sandra Alves, Renata Wassermann, Flavio L. C. de Moura 23 and 24 September 2017 Proof eXchange for Theorem Proving (PxTP) Catherine Dubois, Bruno Woltzenlogel Paleo 23 and 24 September 2017 EPS - Encyclopedia of Proof Systems Giselle Reis, Bruno Woltzenlogel Paleo 24 and 25 September 2017 DaLi - Dynamic Logic: new trends and applications Mario Benevides, Alexandre Madeira 24 September 2017 Tutorials: General methods in proof theory for modal and substructural logics Bjoern Lellmann, Revantha Ramanayake 23 September 2017 From proof systems to complexity bounds Anupam Das 24 September 2017 Proof Compressions and the conjecture NP =3D PSPACE Lew Gordeev, Edward Hermann Haeusler 25 September 2017 PVS for Computer Scientists Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato 25 September 2017 Details will be published in separate calls and on the conference website. PROGRAM COMMITTEE CHAIRS Mauricio Ayala-Rincon, U. Brasilia Cesar Munoz, NASA PROGRAM COMMITTEE Maria Alpuente, T.U. Valencia Vander Alves, U. Brasilia June Andronick, Data61, CSIRO, UNSW Jeremy Avigad, Carnegie Mellon U. Sylvie Boldo, INRIA LRI Ana Bove, Chalmers & Gothenburg U. Adam Chlipala, MIT Gilles Dowek, INRIA, ENS Cachan Aaron Dutle, NASA Amy Felty, U. Ottawa Marcelo Frias, I.T. Buenos Aires Ruben Gamboa, U. Wyoming Herman Geuvers, Radboud U. Elsa Gunter, U. Illinois U.C. John Harrison, Intel Corporation Nao Hirokawa, JAIST Matt Kaufmann, U. Texas Austin Mark Lawford, McMaster U. Andreas Lochbihler, ETH Zurich Assia Mahboubi, INRIA Panagiotis Manolios, Northeastern U. Gopalan Nadathur, U. Minnesota Keiko Nakata, SAP Potsdam Adam Naumowicz, U. Bialystok Tobias Nipkow, T.U. Munich Scott Owens, U. Kent Sam Owre, SRI Lawrence Paulson, U. Cambridge Leila Ribeiro, U.F. Rio Grande do Sul Claudio Sacerdoti Coen, U. Bologna Augusto Sampaio, U.F. Pernambuco Monika Seisenberger, Swansea U. Christian Sternagel, U. Innsbruck Sofiene Tahar, Concordia U. Christian Urban, King's College London Josef Urban, Czech T.U. Prague CONTACT INFORMATION itp2017@easychair.org http://itp2017.cic.unb.br --- To opt-out from this mailing list, send an email to fm-announcements-request@lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-owner@lists.nasa.gov