Tue 18 Jan 2022 06:05 - 06:35 at PEPM - Contributed Talks 2 Chair(s): Jonathan Immanuel Brachthäuser

Let insertion in program generation is producing code with definitions (let-statements). Although definitions precede uses in generated code, during code generation ‘uses’ come first: we might not even know a definition is needed until we encounter a reoccuring expression. Definitions are thus generated ‘in hindsight’, which explains why this process is difficult to understand and implement~– even more so for parameterized, recursive and mutually recursive definitions.

We have earlier presented an interface for let(rec) insertion– i.e. for generating (mutually recursive) definitions. We demonstrated its expressiveness and applications, but not its implementation, which relied on effects and compiler magic.

We now show how one can understand let insertion, and hence implement it in plain OCaml. We give the first denotational semantics of let(rec)-insertion, which does not rely on any effects at all. The formalization guided the implementation of let(rec) insertion in the current version of MetaOCaml.

Tue 18 Jan

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

05:20 - 06:35
Contributed Talks 2PEPM at PEPM
Chair(s): Jonathan Immanuel Brachthäuser University of Tübingen
Two-level Just-in-Time Compilation with One Interpreter and One EngineRemote
Yusuke Izawa Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology, Carl Friedrich Bolz-Tereick Heinrich-Heine-Universität Düsseldorf
Pre-print Media Attached File Attached
let (rec) insertion without Effects, Lights or MagicRemote
Oleg Kiselyov Tohoku University, Japan, Jeremy Yallop University of Cambridge