From: Tarmo Uustalu <tarmo@cs.ioc.ee>
To: categories@mta.ca
Subject: TYPES 2015 call for participation
Date: Fri, 1 May 2015 23:57:05 +0300 [thread overview]
Message-ID: <E1YoL0a-0001Ng-El@mlist.mta.ca> (raw)
* 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åstad (1992), Nijmegen (1993),
Båstad (1994), Torino (1995), Aussois (1996), Kloster Irsee (1998),
Lökeberg (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
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ònoma 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
Contributed talks
See the programme at
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.
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à 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ëlle Despeyroux (INRIA Sophia Antipolis - Méditerranée)
Herman Geuvers (Radboud Universiteit Nijmegen)
Sam Lindley (University of Edinburgh)
Assia Mahboubi (INRIA Saclay - Île-de-France)
Ralph Matthes (IRIT, CNRS and Université Paul Sabatier)
Aleksandar Nanevski (IMDEA Software)
Christine Paulin-Mohring (LRI, Université Paris-Sud)
Simona Ronchi Della Rocca (Università di Torino)
Ulrich Schöpp (Ludwig-Maximilians-Universität München)
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/ ]
reply other threads:[~2015-05-01 20:57 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=E1YoL0a-0001Ng-El@mlist.mta.ca \
--to=tarmo@cs.ioc.ee \
--cc=categories@mta.ca \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).