Sequent calculus as a compiler intermediate language

  • Paul Downen ,
  • Luke Maurer ,
  • Zena Ariola ,
  • Simon Peyton Jones

International Conference on Functional Programming (ICFP'16) |

Published by ACM

The lambda-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 be a good intermediate language, too? To explore this question we designed Sequent Core, a practically-oriented variant of sequent calculus, and used it to re-implement a substantial chunk of the Glasgow Haskell Compiler.