Summer School on Generic and Effectful Programming

St Anne's College, Oxford, 6th to 10th July 2015

About

Generic programming is a technique that exploits the inherent structure that exists in data, to automatically produce efficient and flexible algorithms that can be adapted to suit different needs. The goal of this school is to explore datatype-generic programming and related topics from a variety of different angles, emphasizing in particular the interplay of generics and effects.

This summer school is the closing activity of the EPSRC-funded project "Unifying Theories of Generic Programming" at Oxford University.

Registration

Register via the Oxford University On-line Store.

Lecturers

I am a Lecturer in Computer Science at the University of St Andrews, interested in type theory, dependently typed functional programming, compilers and domain specific languages (DSLs). I am currently working on the implementation of DSLs for stateful, resource-aware programming, especially for correct network protocol design and implementation, using Idris, a dependently typed functional programming language.

When I’m not doing that, you might find me playing Go (I’m about 1 kyu), walking up a hill, watching a game of cricket, or waiting for a delayed train.

I’m afraid I also perpetrated the whitespace programming language.

Fritz Henglein's research interests are in semantic, logical and algorithmic aspects of programming languages, specifically type inference, type-based program analysis, algorithmic functional programming and domain-specific languages, and the application of programming language technology, presently in enterprise systems (Project 3gERP and health care process modeling (Project TrustCare).

After undergraduate studies at Technische Universität München, he obtained his Ph.D. from Rutgers University and joined New York University, Utrecht University and DIKU, the Department of Computer Science at the University of Copenhagen. After starting Hafnium ApS to keep the Y2K bug at bay and being on the start-up faculty of the IT University of Copenhagen to increase IT proficiency, he rejoined DIKU as professor with special duties in programming languages. He is now head of the algorithms and programming languages group at DIKU. His goal is to contribute to the development of software that comes with technical and legal guarantees of having no defects (which should be considered a very modest ambition indeed).

I am a Haskell consultant and co-owner of Well-Typed LLP, living in Regensburg, Germany. My first exposure to functional programming was during his undergraduate studies in Mathematics and Computer Science at the University of Konstanz. Inspired by that, I did a PhD on datatype-generic programming in Haskell at Utrecht University, which I completed in 2004. After being a postdoc and lecturer in Tallinn, Freiburg, Bonn, and Utrecht, I joined Well-Typed in 2010.

I am very interested in applying functional programming to real-world problems, and in particular in designing a programming language and its type system such that it facilitates code reuse and code evolution. To me, datatype-generic programming is an important technique to achieve these goals. Other research interests of mine include domain-specific languages, dependent types, parallel and concurrent programming, and version control.

At Well-Typed, I'm working on various projects for companies that use Haskell, as well as on open-source Haskell projects. I enjoy finding many opportunities to apply Computer Science research (other people's as well as mine) in practice. I am also responsible for designing and developing our Haskell training courses.

Conor McBride (University of Strathclyde)
on Datatypes of Datatypes

Conor McBride is a Lecturer in Computer Science. His research is centred on the design of type systems for dependently typed programming, a topic in which his relentless failure continues to stir others to success. He was partly responsible for the programming language Epigram, which was hated sufficiently vigorously by its users that they built Agda 2 and Idris instead. His preprocessor, the Strathclyde Haskell Enhancement, was in such poor taste that the Glasgow Haskell Compiler had to be extended with native facilities for dependently typed programming. His current interests include first class notions of datatype description and operations over them, coinduction, effect systems, information flow systems, and interminable wrangling about equality. He does these things badly so that you can do them better.

I am a Principal Researcher at Microsoft Research, Cambridge. I help Microsoft make better programming languages, and, through that, make people more productive and happier.

My main current responsibility is the design and implementation of F# (blog), though I've also worked on C# (being co-responsible for C# and .NET generics) and, indirectly, Visual Basic and other .NET languages.

As a researcher, my area is programming language design and implementation, with emphasis on making functional languages that are simpler to use, interoperate well with other languages and which incorporate aspects of object-oriented, asynchronous and parallel programming. I am interested in programming language perspectives on type inference, concurrency, reactivity, pattern matching and language-oriented programming. I also work extensively with teams in the Microsoft Developer Division on other programming-related technologies.

I am the primary author of Expert F#, published in 2007, and we are now working on a second edition of this book. In the past I have worked in formal specification, interactive proof, automated verification and proof description languages. I have a PhD from the University of Cambridge and am a member of the WG2.8 working group on functional programming.

Tarmo Uustalu (Tallinn University of Technology)
on Containers for Effects and Contexts

I am a leading researcher and head of the logic and semantics group of the Institute of Cybernetics (IoC) in Tallinn. I am interested in proof theory and type theory, functional programming (dependently typed programming), category theory (coalgebra), type systems, program logics, program analysis and transformations. My MSc is from the Tallinn University of Technology (1992) and my PhD from KTH Royal Institute of Technology in Stockholm (1998). In 2000-2002 I was a postdoc at the University of Minho in Braga. Since the return from Portugal, I have worked at IoC.

Dates and venues

Registration deadline: 21st June 2015

School: 6th to 10th July 2015, St Anne's College (directions)

Dinner: 8th July 2015, Balliol College (directions). 6:30 pm drinks reception, 7:15pm dinner.

Prerequisites

The school is aimed at doctoral students in programming languages and related areas; however, researchers and practitioners will be very welcome, as will strong masters students with the support of a supervisor. It will be assumed that participants have a good understanding of typed functional programming, as in Haskell, O'Caml, or F#.

Costs

Costs will be kept low, thanks to support from EPSRC. There will be a nominal registration fee of £135, and B&B accommodation in college will be £75 (ensuite) or £48 (shared bathroom) per night. We can accept at most 50 participants; places will be allocated on a first-come, first-served basis.

Further information

For further information, please contact Elizabeth Walsh.