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
Times are displayed in time zone: Osaka, Sapporo, Tokyo change

13:40 - 14:55
Session 2Research Papers at Noh Theater
Chair(s): Kathleen FisherTufts University
13:40
25m
Talk
A New Verified Compiler Backend for CakeML
Research Papers
Yong Kiam TanIHPC at A*STAR, Singapore, Magnus O. MyreenChalmers University of Technology, Sweden, Ramana KumarData61 at CSIRO, Australia, Anthony FoxUniversity of Cambridge, UK, Scott OwensUniversity of Kent, UK, Michael NorrishData61 at CSIRO, Australia
DOI
14:05
25m
Talk
Sequent Calculus as a Compiler Intermediate Language
Research Papers
Paul DownenUniversity of Oregon, USA, Luke MaurerUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft Research, UK
DOI
14:30
25m
Talk
Refinement through Restraint: Bringing Down the Cost of Verification
Research Papers
Liam O'ConnorUNSW, Australia, Zilin ChenUNSW, Australia, Christine RizkallahUniversity of Pennsylvania, USA, Sidney AmaniUNSW, Australia, Japheth LimData61, Australia, Toby MurrayUniversity of Melbourne, Australia, Yutaka NagashimaData61, Australia, Thomas SewellUNSW, Australia, Gerwin KleinUNSW, Australia
DOI