From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8610 Path: news.gmane.org!not-for-mail From: Tarmo Uustalu Newsgroups: gmane.science.mathematics.categories Subject: TYPES 2015 call for participation Date: Fri, 1 May 2015 23:57:05 +0300 Message-ID: Reply-To: Tarmo Uustalu NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1430525479 26711 80.91.229.3 (2 May 2015 00:11:19 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sat, 2 May 2015 00:11:19 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Sat May 02 02:11:11 2015 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.127]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1YoL1S-00048C-66 for gsmc-categories@m.gmane.org; Sat, 02 May 2015 02:11:10 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:38147) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1YoL0a-0006yd-8t; Fri, 01 May 2015 21:10:16 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1YoL0a-0001Ng-El for categories-list@mlist.mta.ca; Fri, 01 May 2015 21:10:16 -0300 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8610 Archived-At: * Invited talks: Andrej Bauer, Gilles Barthe, Peter Selinger * Tutorials: Joachim Kock, Peter LeFanu Lumsdaine * Registration closes 8 May 2015. CALL FOR PARTICIPATION 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. Invited=20 Gilles Barthe (IMDEA Software) Computer-aided cryptography Andrej Bauer (University of Ljubljana) The troublesome reflection rule Peter Selinger (Dalhousie University) Types for quantum computing Tutorials Joachim Kock (Universitat Aut=C3=B2noma de Barcelona) Polynomial functors: a general framework for induction and substitution Peter LeFanu Lumsdaine (Stockholm University) Higher inductive types: what we understand, what we don't=20 Contributed talks See the programme at=20 http://cs.ioc.ee/types15/programme.html Host city and venue Tallinn, on the shores of the Gulf of Finland, is famous for its medieval Old Town. The conference will take place at the historic House of the Blackheads in the middle of the Old Town. =20 The welcome reception of the conference will be at the spectacular Seaplane Harbour, which received a special commendation from the 2014 European Museum of the Year competition. Registration Please register online by 8 May 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, CNRS and Universit=C3=A9 Paul Sabatier) Aleksandar 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 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]