Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX. - Vadim Zaliva; Ilia Zaichuk; Franz Franchetti (VSTTE, 2020)

Modular, compositional, and executable formal semantics for LLVM IR. - Yannick Zakowski; Calvin Beck; Irene Yoon 001; Ilia Zaichuk; Vadim Zaliva; Steve Zdancewic (Proc. ACM Program. Lang., 2021)