Noninterference for free. - William J. Bowman; Amal Ahmed 001 (ICFP, 2015)

Profile-guided meta-programming. - William J. Bowman; Swaha Miller; Vincent St-Amour; R. Kent Dybvig (PLDI, 2015)

Fully abstract compilation via universal embedding. - Max S. New; William J. Bowman; Amal Ahmed 001 (ICFP, 2016)

Typed closure conversion for the calculus of constructions. - William J. Bowman; Amal Ahmed 001 (PLDI, 2018)

Type-preserving CPS translation of Σ and Π types is not not possible. - William J. Bowman; Youyou Cong; Nick Rioux; Amal Ahmed 001 (Proc. ACM Program. Lang., 2018)

Practical Sized Typing for Coq. - Jonathan Chan 002; William J. Bowman (CoRR, 2019)

Dependent type systems as macros. - Stephen Chang 001; Michael Ballantyne; Milo Turner; William J. Bowman (Proc. ACM Program. Lang., 2020)

ANF preserves dependent types up to extensional equality. - Paulette Koronkevich; Ramon Rakow; Amal Ahmed 001; William J. Bowman (J. Funct. Program., 2022)

Human Perception-Inspired Grain Segmentation Refinement Using Conditional Random Fields. - Doruk Aksoy; Huolin L. Xin; Timothy J. Rupert; William J. Bowman (CoRR, 2023)

Is sized typing for Coq practical? - Jonathan Chan 002; Yufeng Li; William J. Bowman (J. Funct. Program., 2023)

Type Universes as Allocation Effects. - Paulette Koronkevich; William J. Bowman (CoRR, 2024)

A Low-Level Look at A-Normal Form. - William J. Bowman (Proc. ACM Program. Lang., 2024)

Indexed Types for a Statically Safe WebAssembly. - Adam T. Geller; Justin Frank; William J. Bowman (Proc. ACM Program. Lang., 2024)

ACM Profits Considered Harmful. - William J. Bowman (Commun. ACM, 2024)

The Ethical Compiler: Addressing the Is-Ought Gap in Compilation (Invited Talk). - William J. Bowman (PEPM, 2025)

Type-Preserving Flat Closure Optimization. - Adam T. Geller; Sean Bocirnea; Chester J. F. Gould; Paulette Koronkevich; William J. Bowman (Proc. ACM Program. Lang., 2025)

One Weird Trick to Untie Landin's Knot. - Paulette Koronkevich; William J. Bowman (CoRR, 2025)