Programming and refactoring dependent types

Thursday 8 December 2016, 6.00pm - 8.00pm

The Davidson Building, 5 Southampton Street, London WC2E 7HA.
The nearest underground stations are Covent Garden and Charing Cross.


Andreas Reuleaux


Dependent types have long been known as a means to specify a program's behaviour in a more precise, fine grained manner, than possible in traditional type systems. They are types whose definitions may depend on values. Examples are vectors (as opposed to more traditional lists), and dependent pairs.

Theorem provers like Agda and Coq, as well as more recent programming languages like Idris are based on these ideas, originating in type theory, and unifying the tasks of programming and theorem proving. I will introduce programming with dependent types in the course of several examples from Idris, and motivate why want would want to use them today.

Pi-forall, another small dependently typed programming language, has served us well for exploring ideas about refactorings in our Pire refactoring tool (Pi-forall refactorer). These ideas are well known from existing refactoring tools for Java, C# and many other languages, but we also break new ground in taking into account the possibilities of dependent types.

About the Speaker:

Andreas ReuleauxAndreas Reuleaux is a member of the Programming Languages and Systems group (PLAS) at the University of Kent currently, focussing on dependent types and refactorings in his research. Having worked in industry for more then ten year in various roles in Berlin and Paris, he decided to return to academia, and embark on a PhD.


PDF Icon Programming and refactoring dependent types - Andreas Reuleaux

Watch the video