Adam T. Geller

Ph.D. @ UBC Ongoing

M.Sc. @ UBC 2020

B.Sc. @ UW 2018

I am a PhD Student in the Software Practices Lab at UBC, supervised by William J. Bowman. My research focuses on using type information for doing compiler optimizations safely in low-level languages. My interests include the theory and practice of types and compilers, especially problems related to practical type preservation. I also have experience working on program verification projects, which is something I enjoy.

Outside of grad school, I referee fencing on the US and Canadian national circuits (I also fence, but not nationally). I have a cat, Socrates. I enjoy cooking and baking, when I have time/energy. My time is often wasted watching various sports, TV shows, and movies.

Publications

2024

Indexed Types for a Statically Safe WebAssembly

Adam T. Geller, Justin Frank, and William J. Bowman

Principles of Programming Lanuages (POPL), 2024

Abs PDF DOI: 10.1145/3632922

We present Wasm-prechk, a superset of WebAssembly (Wasm) that uses indexed types to express and check simple constraints over program values. This additional static reasoning enables safely removing dynamic safety checks from Wasm, such as memory bounds checks. We implement Wasm-prechk as an extension of the Wasmtime compiler and runtime, evaluate the run-time and compile-time performance of Wasm-prechk vs WebAssembly configurations with explicit dynamic checks, and find an average run-time performance gain of 1.71x faster in the widely used PolyBenchC benchmark suite, for a small overhead in binary size (7.18% larger) and type-checking time (1.4% slower). We also prove type and memory safety of Wasm-prechk, prove Wasm safely embeds into Wasm-prechk ensuring backwards compatibility, prove Wasm-prechk type-erases to Wasm, and discuss design and implementation trade-offs.