Programme with slides

Special issue on Dependently Typed Programming (DTP 10)

Please submit your papers to a special issue of MSCS on Dependently Typed Programming (DTP 2010) related to the workshop. Edited by Conor McBride and myself. Deadline for submissions 31 January 2011. See full CFP.

Introduction

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 (and even C#) are incorporating some kinds of type-level data.

When types involve data, they can capture relationships between data, internalising invariants necessary for appropriate computation. When data describe types, we can express patterns of programming in code. We're beginning to see how to take advantage of the power and precision which dependent types afford, but there are still plenty of problems to address and issues to resolve. The design space is large: this workshop is a forum for researchers who are lucky enough to be exploring it.

We hope that the workshop will attract people who either work on the design and implementation of dependently typed programming languages and development environments, or who are using existing systems to develop dependently typed programs or libraries. The following list contains an (incomplete) selection of topics relevant for the workshop:

  • The design of dependently typed programming languages: Should we care about phase, or not? Are we going to be partial or total? Are we going to be uniform or properly dependent? How do we deal with equality on the level of types.
  • Programming: What are good examples of dependently typed programming? What are the killer apps? What are the emerging programming patterns?
  • Type checking and elaboration: Clearly, dependent types raise issues which go beyond the traditional Hindley-Milner approach, but hopefully there is a lot to salvage.
  • Compilation: Can we produce efficent code for Dependently Typed Programs? At least as good as C, if not better?
  • Development environments: Dependent types open up new challenges but also new opportunities for IDEs.
  • Reusability: Finer types reduce the reusability of code, but maybe the dependent types come with their own remedy: generic programming using universes? Do we need a module system, and if yes how should it look like? What are examples of good library design?
  • Reasoning: How well do dependent types integrate with reasoning? Or is program verification just a special form of programming anyway?
  • Totality: Should dependently typed programs be total And if so how do we make sure that they are? (Incidently this is related to the topic of another FLoC workshop: PAR 2010).
  • Effects: How to interface dependently typed programs with the real world?
This workshop is a squel to the previous workshop on dependently typed programming in Nottingham in 2008: DTP 2008.

Organizers

Thorsten Altenkirch and Conor McBride.

Invited speakers

Ana Bove (Chalmers)
Matthieu Sozeau (Harvard University)

Format

The workshop will have two invited talks and however many contributed talks you contribute. We expect there will be plenty of time for discussion. If you want to volunteer a talk or a demo at the workshop, please send us a title and abstract before 4 June 2010 to dtp10@cs.nott.ac.uk. Slots will be at least 30 minutes (unless you ask for less), and we hope to fit everyone in. Please let us know wether you want to give a talk (with title) before 16 April 2010,Clearly, if we're overwhelmed, we'll be very pleased, and we'll have to think again. We plan to organize a special issue of Fundamenta Informaticae to contain refereed papers related to the topic of the workshop.

Over to You

If you want to talk please send us title and abstract before the deadline. Registration is via FLoC.

Preliminary Programme