Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)
Please note the unusual day for this talk; it is on Monday.
|title:||Type-directed compilation in the wild: Haskell and Core|
|speaker:||Simon Peyton Jones|
|time:||Monday, 29 July 2013, 10:30am|
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract: Academic papers often describe typed calculi, but it is rare to find one in a production compiler. Indeed, I think the Glasgow Haskell Compiler (GHC) may be the only production compiler in the world that really has a remorselessly statically-typed intermediate language, informally called "Core", or (when writing academic papers) the more respectable-sounding "System FC".
As real compilers go, GHC's Core language is tiny: it is a slight extension of System F, with letrec, data types, and case expressions. Yet all of Haskell (now a bit of a monster) gets translated into it. In the last few years we have added one new feature to Core, namely typed (but erasable) coercions that witness type equalities, which turn Core into a particular kind of proof-carrying code. This single addition has opened the door to a range of source-language extensions, such as GADTs and type families.
In this talk I'll describe Core, and how it has affected GHC's development over the last two decades, concentrating particularly on recent developments, coercions, evidence, and type families.
To test your mettle I hope to end up with the problem we are currently wrestling with: proving consistency of a non-terminating rewrite system with non-left-linear rules.
bio: Simon Peyton Jones, MA, MBCS, CEng, graduated from Trinity College Cambridge in 1980. After two years in industry, he spent seven years as a lecturer at University College London, and nine years as a professor at Glasgow University, before moving to Microsoft Research (Cambridge) in 1998.
His main research interest is in functional programming languages, their implementation, and their application. He has led a succession of research projects focused around the design and implementation of production-quality functional-language systems for both uniprocessors and parallel machines. He was a key contributor to the design of the now-standard functional language Haskell, and is the lead designer of the widely-used Glasgow Haskell Compiler (GHC). He has written two textbooks about the implementation of functional languages.
More generally, he is interested in language design, rich type systems, software component architectures, compiler technology, code generation, runtime systems, virtual machines, and garbage collection. He is particularly motivated by direct use of principled theory to practical language design and implementation -- that's one reason he loves functional programming so much. His home page is at http://research.microsoft.com/~simonpj.