[Caml-list] TYPES 2015 call for contributions

[Tarmo Uustalu <tarmo@cs.ioc.ee>]

                      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å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.

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à 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, Université Paul Sabatier)
Aleks 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