Dependently typed programming is here today: where will it go tomorrow? On the one hand, dependent type theories have grown programming languages; on the other hand, the type systems of programming languages like Haskell, Scala and even C# are incorporating some kinds of type-level data.
The purpose of this workshop is to discuss experiences with dependent types in programming and future developments for dependently-typed languages. Topics of interest include, but are not limited to:
- Language Design, both in the context of possible extensions and modifications of existing languages and the development of new languages with dependent types;
- Theory, such as formal treatments of semantics and type systems;
- Compilation, including implementations and optimization of dependently-typed languages;
- Tools, in the form of IDEs, profilers, tracers, debuggers, and testing tools;
- Functional Pearls, being elegant, instructive examples of using dependent types;
- Experience Reports, general practice and experience with dependently-typed languages, e.g., in an education or industry context.
The workshop will consist of an invited speaker and contributed talks. Talks were be selected according to relevance to the workshop, based on submission of an extended abstract.
The invited speaker will be Alan Jeffrey (Bell Labs, Alcatel-Lucent)
The program is now available.
After the workshop, we plan to invite participants to submit full papers for formal refereeing. Further details will be announced in due course.
- Abstract Submission (DEADLINE EXTENDED) Wednesday, 7th May 2014
- Author Notification by Monday, 12th May 2014
- Workshop Sunday, 13th July 2014
- Edwin Brady (University of St Andrews, Program Chair)
- Thorsten Altenkirch (University of Nottingham, Steering Committee Chair)
- Andreas Abel (Chalmers and Gothenburg University, Sweden)
- Amal Ahmed (Northeastern University, USA)
- Nicola Botta (Postdam Institute for Climate Impact Research, Germany)
- Edwin Brady (University of St Andrews, Chair)
- David Christiansen (IT University of Copenhagen, Denmark)
- Adam Gundry (Well-Typed LLP)
- Dan Licata (Wesleyan University, USA)
- Shin-Cheng Mu (Academia Sinica, Taiwan)
- Hongwei Xi (Boston University, USA)
Registration is open via the Vienna Summer of Logic.
The workshop started as a TYPES topical workshop in 2008 in Nottingham, collocated with LICS in Edinburgh in 2010, ITP in Nijmegen in 2011, and ICFP in Boston in 2013. Closely related seminars were organized at Dagstuhl, Germany in 2004 and Shonan Village, Japan in 2011.