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 SepDisplayed time zone: Osaka, Sapporo, Tokyo change
Mon 19 Sep
Displayed time zone: Osaka, Sapporo, Tokyo change
13:40 - 14:55 | |||
13:40 25mTalk | 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 25mTalk | 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 25mTalk | 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 | ||