!NEW! SlidesThe programme now contains links to many of the slides, thanks to the authors who have provided these! (you can also look at the Abstracts still).
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?
- Effects: How to interface dependently typed programs with the real world? While this was the topic of our recent sister workshop, we may want to continue this theme here.
OrganizersThorsten Altenkirch, Peter Morris and Tarmo Uustalu.
Invited speakerLennart Augustsson (Credit Suisse)
Xavier Leroy (INRIA Rocquencourt)
ParticipantsJohan Jeuring, Jeremy Gibbons, Vincent Siles, Ralph Matthes, Noam Zeilberger, Tarmo Uustalu, Yangyue FENG, seokhyun han, Bruno Bernardo, Ulf Norrell, Bruno Barras, Adam Poswolsky, Randy Pollack, Varmo Vene, Stephanie Weirich, Shin-Cheng Mu, Sean Wilson, Arnaud Spiwack, Andrés Sicard-Ramírez, Xavier Leroy, Lennart Augustsson, Edwin Brady, Mathieu Boespflug , Gilles Barthe, Benjamin Gregoire, Colin Riba, Jorge-Luis Sacchini, Matthieu Sozeau, Hsiang-Shang Ko, Anton Setzer, Chris Stork, James McKinna, James Chapman, Conor McBride, Thorsten Altenkirch, Peter Morris, Neil Sculthorpe, Henrik Nilsson, Nicolas Oury, Wouter Swierstra, Nils Danielsson, James McKinna, Andreas Abel, Sebastian Hanowksy This list is not updated automatically.
The workshop was held at the National College for School Leadership Learning and Conference Centre, in the Jubilee Campus of the University of Nottingham, from Monday 18 February to Wednesday 20 February. Thanks to everyone who attended and made it such a wonderful meeting.
Below is a map of a few important locations, the NCSL is green, the P&J Blue and the Three Wheatsheves Yellow. The route of the Rainbow 4 & 5 buses is also shown in purple, these run from very close to the station (also marked if you scroll East):
View Larger Map