Simon Peyton-Jones (Microsoft Research, UK) joint invited speaker for TLCA 2013 and RTA 2013
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.
(Source
of this text.)
Jarkko Kari (University of Turku, Finland) invited speaker for RTA 2013.
Jarkko J. Kari is a Finnish mathematician and computer scientist,
known for his contributions to the theory of Wang tiles and
cellular automata. Kari is currently a professor at the
Department of Mathematics, University of Turku.
He recieved his PhD in 1990 from the Unversity of Turku.
Mitsu Okada (Keio University, Japan) invited speaker for RTA 2013.
Mitsuhiro Okada is a Professor at the
Department of Philosophy of Keio University,
currently working on philosophy, logic, computer science, cognitive
science, and brain science,
and is serving as the director of Global Research Centre for Logic ans
Sensitivity, and the acting director
of Research Centre for Thiking and Behavioral Judgment of Keio
University In computer science field,
his current interests include computational completeness proofs for
cryptographic protocols logical verifications,. diagrammatic inferences,
logico-philosophical roots of modern historical establishment for the
relations between the rewriting and equational calculi such as
Knuth-Bendix completion and
the uniqueness condition, and others.
joint TLCA+RTA invited talk by Simon Peyton-Jones:
Type-directed compilation in the wild: Haskell and Core
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 strongly-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. 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. I'll also mention the role of user-written rewrite rules as a compiler extension mechanism. Overall, I will try to give a sense of the ways in which the work of the typed lambda-calculi and rewriting communities has influenced at least one real compiler.
Home RTA 2013 | Invited Speakers | Accepted Papers | Programme Committee | Steering Committee | Call for Papers
Home RDP 2013 | Call for Workshops for RDP 2013 | Organizing Committee of RDP 2013