It's always nice to see the papers that come out of Tiark Rompf's group. For background, here are some other great ones:

Lightweight Modular Staging: A Pragmatic Approach to Runtime Code Generation and Compiled DSLs https://infoscience.epfl.ch/record/150347/files/gpce63-rompf...

Collapsing Towers of Interpreters: https://www.cs.purdue.edu/homes/rompf/papers/amin-popl18.pdf

LMS-Verify: Abstraction Without Regret for Verified Systems Programming: http://lampwww.epfl.ch/~amin/pub/lms-verify.pdf

There's a ton more. Nada Amin's talks on the last two papers are excellent also:

https://www.youtube.com/watch?v=QuJ-cEvH_oI https://www.youtube.com/watch?v=Ywy_eSzCLi8

Oh, and I forgot my favorite: Functional Pearl: A SQL to C Compiler in 500 Lines of Code https://www.cs.purdue.edu/homes/rompf/papers/rompf-icfp15.pd...

Some really mind-blowing stuff.