Staging with Control: Type-Safe Multi-stage Programming with Control Operators
Staging allows a programmer to write domain-specific, custom code generators. Ideally, a programming language for staging provides all necessary features for staging, and at the same time, gives static guarantee for the safety properties of generated code including well typedness and well scopedness. We address this classic problem for the language with control operators, which allow code optimizations in a modular and compact way. Specifically, we design a staged programming language with the expressive control operators shift0 and reset0, which let us express, for instance, multi-layer let-insertion, while keeping the static guarantee of well typedness and well scopedness. For this purpose, we extend our earlier work on refined environment classifiers which were introduced for the staging language with state. We show that our language is expressive enough to express interesting code generation techniques, and that the type system enjoys type soundness. We also mention a type inference algorithm for our language under reasonable restriction.
this URL might only work when visiting from a http://www.sigplan.org/ URL.
Mon 23 OctDisplayed time zone: Tijuana, Baja California change
10:30 - 12:00 | |||
10:30 25mTalk | Refining Semantics for Multi-stage Programming GPCE 2017 DOI Authorizer link | ||
10:55 25mTalk | Staging for Generic Programming in Space and Time GPCE 2017 DOI Authorizer link | ||
11:20 25mTalk | Staging with Control: Type-Safe Multi-stage Programming with Control Operators GPCE 2017 DOI Authorizer link | ||
11:45 15mTalk | Code Staging in GNU GuixShort paper GPCE 2017 Ludovic Courtès Inria, France DOI Authorizer link |