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 8DF3580142; Sat, 20 May 2017 15:42:38 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tarmo@cs.ioc.ee; spf=None smtp.mailfrom=tarmo@cs.ioc.ee; spf=None smtp.helo=postmaster@smtp3.ioc.ee Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of tarmo@cs.ioc.ee) identity=pra; client-ip=193.40.251.188; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="tarmo@cs.ioc.ee"; x-sender="tarmo@cs.ioc.ee"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of tarmo@cs.ioc.ee) identity=mailfrom; client-ip=193.40.251.188; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="tarmo@cs.ioc.ee"; x-sender="tarmo@cs.ioc.ee"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp3.ioc.ee) identity=helo; client-ip=193.40.251.188; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="tarmo@cs.ioc.ee"; x-sender="postmaster@smtp3.ioc.ee"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A2yiTFxCq0ZrbOR4wsxEOUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPTypcbcNUDSrc9gkEXOFd2CrakV1ayL7OigATVGusfe9ihaMdRlbFwst4?= =?us-ascii?q?Y/p08aPIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0Iu?= =?us-ascii?q?frymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMYjIZmK6s90BvEr3lVcO?= =?us-ascii?q?hS2W9kOEifkhj468qy5pJv7zhct/c8/MNcTKv2eLg1QrNfADk6KW4549Hluwfe?= =?us-ascii?q?RgWV/HscVWsWkhtMAwfb6RzxQ4n8vCjnuOdjwSeWJcL5Q6w6VjSk9KdrVQTniD?= =?us-ascii?q?wbOD4j8WHYkdJ/gaRGqx+8vRN/worUYIaINPpie67WYN0XSXZdUstXSidOBZ6y?= =?us-ascii?q?b5YUD+oZI+lXs5X9qVUJrRu7HwasBeXvwSJMinL52aA21uIsGhzE0gM9BdIDqH?= =?us-ascii?q?raotXrOqkPUu67y6bHwinMYf5NxTfw6pLFfgw7rP2QQ759d9fax0k1FwPCi1Wd?= =?us-ascii?q?sZLrMCmP1uQItGiQ8uRvVf+0i247sQ5xpiWvzdorh4nVnI0V0FXE9SJizYkpPt?= =?us-ascii?q?20Uk97Ydm4H5dKqS6VKZJ7T8U/SG9mvyY6z6cJuZ+9fCUSx5QnwBnfa/ODc4eW?= =?us-ascii?q?+B7sSOGRITJ+iXl4e7y/nw6//VWkx+DyTMW530pGojBbntTMq3wBzQHf58uER/?= =?us-ascii?q?Z740yvwyyA1xrJ5eFBOU00lbTUK5omwrMojZoTtFjDHjf4lUnsja+WcVkr9vK2?= =?us-ascii?q?5Ov5ernmp5mcOJFoigzmL6gjnsKyDf43PwQSRWSX5+Sx2KD58UHkQ7hHjeU6kq?= =?us-ascii?q?zDv5DbIcQbqLS5AwhQ0os79xawFS2m0NEfnXQcMF1FYwiLj4nuO17SOvz3E+mw?= =?us-ascii?q?j0y2kDh33/DGIqHhApLVI3ffirjheLJ951dYyAoy1tBf+4lZCqoBIfL2Qk/+rs?= =?us-ascii?q?bUDh4/MwyuwuboEs9x1o0EWWiXGK+WLLvSsUOU5uIoO+SDeIgVuC/kJ/c54/7u?= =?us-ascii?q?kGQ2lEQGfaip2JsXcGq3Eu5nI0Wfe3rsg80OHX0EvgokH6TWjwiJVicWbHKvVY?= =?us-ascii?q?o94Cs6AcSoF8OLTYmohPmF3TynNpxQfGFPTF6WVT/heImNc/MNcz6JZMRhmzgB?= =?us-ascii?q?WKK6DZQshj+0swqv97N9K+2cxzADqZvnyZAh++TJkBYa/icyDsOWlWyAGTIn1l?= =?us-ascii?q?gUTiM7ifgs6Xd2zU2OhPQpjg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CvAwDhRiBZ/7z7KMFcHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgwGBC5AGqQMsgkKJeRQBAQEBAQEBAQEBAWoogjMMgn0dezRPJwe?= =?us-ascii?q?HdgGCFQq0PIsjIQWKZUOEc4YSBZEpjG2HHYt1eYEZhTyKL4hwiEgMgwQ2IUw+L?= =?us-ascii?q?yAIL4J6hEU9iUMBAQE?= X-IPAS-Result: =?us-ascii?q?A0CvAwDhRiBZ/7z7KMFcHAEBBAEBCgEBFwEBBAEBCgEBgwG?= =?us-ascii?q?BC5AGqQMsgkKJeRQBAQEBAQEBAQEBAWoogjMMgn0dezRPJweHdgGCFQq0PIsjI?= =?us-ascii?q?QWKZUOEc4YSBZEpjG2HHYt1eYEZhTyKL4hwiEgMgwQ2IUw+LyAIL4J6hEU9iUM?= =?us-ascii?q?BAQE?= X-IronPort-AV: E=Sophos;i="5.38,369,1491256800"; d="scan'208";a="224317233" Received: from smtp3-out.ioc.ee (HELO smtp3.ioc.ee) ([193.40.251.188]) by mail3-smtp-sop.national.inria.fr with ESMTP; 20 May 2017 15:42:37 +0200 Received: from cs.ioc.ee (ioc-gw.kybi [172.17.0.254]) by smtp3.ioc.ee (Postfix) with ESMTPSA id 36E2540893; Sat, 20 May 2017 16:42:36 +0300 (EEST) Date: Sat, 20 May 2017 16:42:36 +0300 From: Tarmo Uustalu To: coq-club@inria.fr, caml-list@inria.fr, agda@lists.chalmers.se Message-ID: <20170520164236.459035f3@cs.ioc.ee> X-Mailer: Claws Mail 3.8.0 (GTK+ 2.24.10; x86_64-pc-linux-gnu) Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Validation-by: tarmo@cs.ioc.ee Subject: [Caml-list] EUTYPES summer school in Ohrid, call for applications COST action CA15123 EUTYPES Summer School on Types for Programming and Verification Ohrid, Macedonia, 10-14 July 2017 https://sites.google.com/view/summerschool2017-eutypes/ CALL FOR APPLICATIONS BACKGROUND Types are pervasive in programming and information technology. A type defines a formal interface between software components, allowing the automatic verification of their connections, and greatly enhancing the robustness and reliability of computations and communications. In rich dependent type theories, the full functional specification of a program can be expressed as a type. Type systems have rapidly evolved over the past years, becoming more sophisticated, capturing new aspects of the behaviour of programs and the dynamics of their execution. The aim of this summer school is to provide advanced training, especially to PhD students and early-career researchers, in all aspects of the theory and practice of type theory and applications. LECTURERS AND COURSES Silvia Ghilezan (University of Novi Sad, Serbia), Aleksy Schubert (Warsaw University, Poland): Untyped, typed lambda calculus, pure type systems Robbert Krebbers (Tehnical University Delft, The Netherlands): The Coq proof assistant for proving and programming Conor McBride (University of Strathclyde): Dependently typed programming, Agda Andrei Paskevich (LRI, France): Program verification in Why3 Thorsten Altenkirch (University of Nottingham, UK): Introduction to homotopy type theory APPLICATION The capacity of the summer school is up to 40 students. 6 nights accommodation costs 228 EUR. A maximum of 30 students (PhD students / early-career researchers) from countries involved in EUTYPES can receive a grant from the COST action to partially cover their costs. To apply for a place in the school and a grant, please fill out the form on the school website; please do so as soon as possible. Application deadline: 2 June 2017. Notification of acceptance and funding: continuously, at the latest by 9 June 2017. VENUE Ohrid is a small town on Lake Ohrid in Macedonia, southwest of Skopje. Ohrid is notable for once having had 365 churches, one for each day of the year, and has been referred to as the Jerusalem of the Balkans. Ohrid and Lake Ohrid are on UNESCO's lists of cultural and natural World Heritage sites. The school will be held in the Congress Centre of Ohrid, which is also the accommodation site. TRAVEL Most participants will have to fly to Skopje and then get to Ohrid by bus. WizzAir operates direct flights to Ohrid from Basel-Mulhouse-Freiburg and London Luton. ORGANIZERS Herman Geuvers, Marija Mihova, Tarmo Uustalu