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 sympa.inria.fr (Postfix) with ESMTPS id 297407FBEB for ; Wed, 14 Jan 2015 19:00:12 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of tarmo@cs.ioc.ee) identity=pra; client-ip=193.40.251.3; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="tarmo@cs.ioc.ee"; x-sender="tarmo@cs.ioc.ee"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of tarmo@cs.ioc.ee) identity=mailfrom; client-ip=193.40.251.3; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="tarmo@cs.ioc.ee"; x-sender="tarmo@cs.ioc.ee"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@postiljon.ioc.ee) identity=helo; client-ip=193.40.251.3; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="tarmo@cs.ioc.ee"; x-sender="postmaster@postiljon.ioc.ee"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhkBAMCttlTBKPsDl2dsb2JhbABbg1iDXcJ7hXWBGEMBAQEBAREBAQEBAQgWB0KEMAZFETUCBSECES2IZL1ElCEBKxiBCYsoglhYgm+BQQWSB4VHjByFXwKCMYFhgXCBQAEBAQ X-IPAS-Result: AhkBAMCttlTBKPsDl2dsb2JhbABbg1iDXcJ7hXWBGEMBAQEBAREBAQEBAQgWB0KEMAZFETUCBSECES2IZL1ElCEBKxiBCYsoglhYgm+BQQWSB4VHjByFXwKCMYFhgXCBQAEBAQ X-IronPort-AV: E=Sophos;i="5.07,757,1413237600"; d="scan'208";a="117038246" Received: from postiljon.ioc.ee ([193.40.251.3]) by mail2-smtp-roc.national.inria.fr with ESMTP; 14 Jan 2015 19:00:11 +0100 Received: from localhost (butler.kybi [172.17.0.12]) by postiljon.ioc.ee (Postfix) with ESMTP id 589EA244E5FB; Wed, 14 Jan 2015 20:00:11 +0200 (EET) X-Virus-Scanned: Debian amavisd-new at ioc.ee Received: from postiljon.ioc.ee ([172.17.0.3]) by localhost (butler.kybi [172.17.0.12]) (amavisd-new, port 10024) with ESMTP id 3s7moU564t+f; Wed, 14 Jan 2015 20:00:06 +0200 (EET) Received: from duality (kybi.ioc.ee [193.40.251.4]) (using TLSv1 with cipher DHE-RSA-AES128-SHA (128/128 bits)) (No client certificate requested) by postiljon.ioc.ee (Postfix) with ESMTPS id 03265244E5F6; Wed, 14 Jan 2015 20:00:06 +0200 (EET) Date: Wed, 14 Jan 2015 20:00:03 +0200 From: Tarmo Uustalu To: caml-list@inria.fr Cc: tarmo@cs.ioc.ee Message-ID: <20150114200003.08b8965b@duality> X-Mailer: Claws Mail 3.8.0 (GTK+ 2.24.10; i686-pc-linux-gnu) Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Validation-by: tarmo@cs.ioc.ee Subject: [Caml-list] TYPES 2015 call for contributions CALL FOR CONTRIBUTIONS 21st International Conference on Types for Proofs and Programs, TYPES 2015 Tallinn, Estonia, 18-21 May 2015 http://cs.ioc.ee/types15/ Background The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalized and computer assisted reasoning and computer programming. The meetings from 1990 to 2008 were annual workshops of a sequence of five EU funded networking projects. Since 2009, TYPES has been run as an independent conference series. Previous TYPES meetings were held in Antibes (1990), Edinburgh (1991), B=C3=A5stad (1992), Nijmegen (1993), B=C3=A5stad (1994), Torino (1995), Aussois (1996), Kloster Irsee (1998), L=C3=B6keberg (1999), Durham (2000), Berg en Dal near Nijmegen (2002), Torino (2003), Jouy en Josas near Paris (2004), Nottingham (2006), Cividale del Friuli (2007), Torino (2008), Aussois (2009), Warsaw (2010), Bergen (2011), Toulouse (2013), Paris (2014). The TYPES areas of interest include, but are not limited to: foundations of type theory and constructive mathematics; applications of type theory; dependently typed programming; industrial uses of type theory technology; meta-theoretic studies of type systems; proof assistants and proof technology; automation in computer-assisted reasoning; links between type theory and functional programming; formalizing mathematics using type theory. We encourage talks proposing new ways of applying type theory. Invited speakers Gilles Barthe (IMDEA Software) Andrej Bauer (University of Ljubljana) Peter Selinger (Dalhousie University) Contributed talks We solicit contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pp formatted with easychair.cls. Submission is via EasyChair by 13 March 2015. The authors will be notified of acceptance/rejection by 3 April 2015. Camera-ready versions of the accepted contributions, due by 24 April 2015, will be published in an informal book of abstracts for distribution at the workshop. Post-proceedings Similarly to TYPES 2011, 2013, 2014, we intend to publish a post-proceedings volume in the Leibniz International Proceedings in Informatics (LIPiCS) series (subject to successful negotiation with Dagstuhl Publishing). Submission to that volume would be open for everyone. Tentative submission deadline: mid-September 2015. Programme committee Andrea Asperti (Universit=C3=A0 di Bologna) Robert Atkey (University of Edinburgh) Ulrich Berger (Swansea University) Jean-Philippe Bernardy (Chalmers University of Technology) Edwin Brady (University of St Andrews) Jo=C3=ABlle Despeyroux (INRIA Sophia Antipolis - M=C3=A9diterran=C3=A9e) Herman Geuvers (Radboud Universiteit Nijmegen) Sam Lindley (University of Edinburgh) Assia Mahboubi (INRIA Saclay - =C3=8Ele-de-France) Ralph Matthes (IRIT, Universit=C3=A9 Paul Sabatier) Aleks Nanevski (IMDEA Software) Christine Paulin-Mohring (LRI, Universit=C3=A9 Paris-Sud) Simona Ronchi Della Rocca (Universit=C3=A0 di Torino) Ulrich Sch=C3=B6pp (Ludwig-Maximilians-Universit=C3=A4t M=C3=BCnchen) Bas Spitters (Carnegie Mellon University) Pawel Urzyczyn (University of Warsaw) Tarmo Uustalu (Institute of Cybernetics, Tallinn) (chair) Organizers Logic and semantics group, Institute of Cybernetics, Tallinn Sponsors ERDF via EXCS, the Estonian Centre of Excellence in Computer Science