Tue 22 Oct 2024 14:00 - 14:30 at San Marino - Session 3 on Code Optimizations Chair(s): Lionel Parreaux

Staged computation is a means to achieve maintainability and high performance simultaneously, by allowing a programmer to express domain-specific optimizations in a high-level programming language. Multi-stage programming languages such as MetaOCaml provide a static safety guarantee for generated programs by sophisticated type systems provided that program generators have computational effects. Despite several studies, it remains a challenging problem to design a type-safe multi-stage programming language with advanced features for computational effects. This paper introduces a two-stage programming language with algebraic effects and handlers. Based on two novel principles ‘handlers as future-stage binders’ and ‘handlers are universal’, we design a type system and prove its soundness. We also show that our language is sufficiently expressive to write various effectful staged computations including multi-level let-insertion, which is a key technique to avoid code duplication in staged computation.

Tue 22 Oct

Displayed time zone: Pacific Time (US & Canada) change

14:00 - 15:30
Session 3 on Code OptimizationsGPCE at San Marino
Chair(s): Lionel Parreaux HKUST (The Hong Kong University of Science and Technology)
14:00
30m
Talk
Type-Safe Code Generation With Algebraic Effects and HandlersDistinguished Research Paper Award
GPCE
Kanaru Isoda University of Tsukuba, Ayato Yokoyama University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba
14:30
30m
Talk
Hot Call-Chain Inlining for the Glasgow Haskell Compiler
GPCE
Celeste Hollenbeck University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh
15:00
30m
Talk
Restaging Domain-Specific Languages: A Flexible Design Pattern for Rapid Development of Optimizing Compilers
GPCE
Amir Shaikhha University of Edinburgh