|
Change #22303
2013-07-23
13:18:33
|
create
Calagator::Event
1250464598
Galois tech talk: Type-directed compilation in the wild: Haskell and Core
Roll back
| description |
nil |
→ |
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. |
| end_time |
nil |
→ |
2013-07-29 11:30:00 -0700 |
| id |
nil |
→ |
1250464598 |
| start_time |
nil |
→ |
2013-07-29 10:30:00 -0700 |
| title |
nil |
→ |
Galois tech talk: Type-directed compilation in the wild: Haskell and Core |
| url |
nil |
→ |
http://corp.galois.com/blog/2013/7/23/tech-talk-type-directed-compilation-in-the-wild-haskell-and.html |
| venue_id |
nil |
→ |
202390439 |
|