Publications

• HELIX: Verified compilation of cyber-physical control systems to LLVM IR

  Preprint, 2026. Manuscript under review.

  A verified compiler pipeline that lowers mathematical descriptions of numerical control code to LLVM IR while checking transformations in Rocq.

• Modular, compositional, and executable formal semantics for LLVM IR

  ICFP'21

  A compositional Rocq semantics for LLVM IR built around interaction trees, with an executable interpreter.

• Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX

  VSTTE'20

  A focused account of HELIX's translation from functional operator languages to imperative languages with memory and floating-point computation.

• Formal verification of floating-point number conversion between ASN.1 BER and IEEE 754 binary encodings

  POPL'19 SRC, undergraduate category third place

  A Rocq development for verifying conversion between ASN.1 BER encodings and IEEE 754 floating-point representations.