Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Mon 19 Sep 2016 14:05 - 14:30 at Noh Theater - Session 2 Chair(s): Kathleen Fisher

The λ-calculus is popular as an intermediate language for practical compilers. But in the world of logic it has a lesser-known twin, born at the same time, called the sequent calculus. Perhaps that would make for a good intermediate language, too? To explore this question we designed Sequent Core, a practically-oriented core calculus based on the sequent calculus, and used it to re-implement a substantial chunk of the Glasgow Haskell Compiler.

Mon 19 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

13:40 - 14:55
Session 2Research Papers at Noh Theater
Chair(s): Kathleen Fisher Tufts University
13:40
25m
Talk
A New Verified Compiler Backend for CakeML
Research Papers
Yong Kiam Tan IHPC at A*STAR, Singapore, Magnus O. Myreen Chalmers University of Technology, Sweden, Ramana Kumar Data61 at CSIRO, Australia, Anthony Fox University of Cambridge, UK, Scott Owens University of Kent, UK, Michael Norrish Data61 at CSIRO, Australia
DOI
14:05
25m
Talk
Sequent Calculus as a Compiler Intermediate Language
Research Papers
Paul Downen University of Oregon, USA, Luke Maurer University of Oregon, USA, Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft Research, UK
DOI
14:30
25m
Talk
Refinement through Restraint: Bringing Down the Cost of Verification
Research Papers
Liam O'Connor UNSW, Australia, Zilin Chen UNSW, Australia, Christine Rizkallah University of Pennsylvania, USA, Sidney Amani UNSW, Australia, Japheth Lim Data61, Australia, Toby Murray University of Melbourne, Australia, Yutaka Nagashima Data61, Australia, Thomas Sewell UNSW, Australia, Gerwin Klein UNSW, Australia
DOI