Sexy Types – Are We Done Yet?


April 15, 2011


Satnam Singh, Simon Payton-Jones, Ulf Norell, Francois Pottier, Erik Meijer, and Conor McBride


MSRC, MSR, Chalmers University, INRIA, University of Strathclyde


Functional programming languages have been a very productive laboratory for developing new language features and in particular powerful type systems. The use of static typing represents the most widespread and successful application of formal verification. Many of the innovations in research languages like Haskell can traced to new features in mainstream programming languages like C#. What will be the new wave of innovations in types that will appear in mainstream languages? Exciting candidates include features like dependent types and linear types and special support for security. Or have we now reached a fix point in the development of type systems? Are some of the latest developments in the type systems of languages like Haskell, Scala and Agda also candidates for adoption by mainstream languages? Have the most recent developments in type systems attained a level of complexity that puts them out of the reach of mainstream programmers?


Satnam Singh, Simon Payton-Jones, Ulf Norell, Francois Pottier, Erik Meijer, and Conor McBride

Prof. Satnam Singh’s research interests include involves finding novel ways to program and use reconfigurable chips called FPGAs and in parallel functional programming. Satnam Singh completed his PhD at the University of Glasgow in 1991 where he devised a new way to program and analyze digital circuits described in a special functional programming language. He then went on to be an academic at the same university and lead several research projects that explored novel ways to exploit FPGA technology for applications like software radio, image processing and high resolution digital printing, and graphics. In 1998 he moved to San Jose California to join Xilinx’s research lab where he developed a language called Lava in conjunction with Chalmers University which allows circuits to be laid out nicely on chips to give high performance and better utilization of silicon resources. In 2004 he joined Microsoft in Redmond Washington where we worked on a variety of techniques for producing concurrent and parallel programs and in particular explored join patterns and software transactional memory. In 2006 he moved to Microsoft’s research laboratory in Cambridge where he works on reconfigurable computing and parallel functional programming. He holds the Chair of Reconfigurable Systems at the University of Birmingham; is a fellow of the IET; a visiting professor at Imperial College; and a visiting lecturer at Chalmers in Gothenburg, Sweden.

François Pottier is a senior researcher at INRIA Paris-Rocquencourt, where he studies programming languages. He is interested in type systems as well as in machine-checked proofs of programs. He hopes, through a combination of these techniques, to make the production of correct software easier and more cost-effective.

Erik Meijer

From Wikipedia, the free encyclopedia
Erik Meijer may refer to:

  • Erik Meijer (politician)
  • Erik Meijer (computer scientist)
  • Erik Meijer (footballer)

I am the Erik Meijer (computer scientist) one from that list.

Conor McBride is a Lecturer in the Department of Computer and Information Sciences at the University of Strathclyde. His PhD thesis, under Rod Burstall, set dependently typed functional programming on a solid theoretical footing. His subsequent work with James McKinna on the Epigram language helped pave the way for the dependently typed language Agda, as well as promoting the uptake of related techniques in less experimental languages such as Haskell and C#. He collaborates with Microsoft Research on dependently typed extensions to Haskell, and is still a creative force at the cutting edge of research in programming with advanced type systems.