Safe and efficient generic functions with MacoCaml
We apply MacoCaml, an extension of OCaml with support for compile-time user-specified code generation, to the generic function problem. MacoCaml’s combination of macros with phase separation and code quotations neatly addresses what is a recurring challenge for OCaml developers: how to write safe and efficient functions over type representations?
Our solution to the challenge also illustrates some recently-established formal guarantees offered by MacoCaml, including soundness and phase distinction.
Sat 9 SepDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:30
|Efficient OCaml compilation with Flambda 2|
|Less Power for More Learning: Restricting OCaml Features for Effective TeachingRemote|
Max Lang Technische Universität München, Nico Petzendorfer Department of Computer Science, Technische Universität München, Garching, GermanyFile Attached
|Osiris: an Iris-based program logic for OCamlRemote|
|Safe and efficient generic functions with MacoCaml|
Dmitrij Szamozvancev University of Cambridge, Leo White Jane Street, Ningning Xie University of Toronto / Google DeepMind, Jeremy Yallop University of CambridgeFile Attached