Adam T. Geller

Software Engineer @ NVIDIA

M.Sc. @ UBC 2020

B.Sc. @ UW 2018

I am a software engineer working on quantum compilation as part of the CUDA-Q team at NVIDIA.

My background and interests are mostly focused on compiler optimizations and type systems. However, I am broadly interested in programming languages, formal verification, and systems. I did a Masters and was several years into my PhD at UBC working on building type systems that support low-level compiler optimizations. In my undergrad, I worked on the Cassius project doing formal verification of webpage layout.

Outside of work, I referee fencing on the US and Canadian national circuits (I also fence a lot). 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.

Recent Publications

2025

Type-Preserving Flat Closure Optimization

Adam T. Geller, Sean Bocirnea, Chester Gould, and 2 more authors

Object-oriented Programming, Systems, Languages and Applications (OOPSLA), 2025

Abs PDF DOI: 10.1145/3720437

Type-preserving compilation seeks to make intent as much as a part of compilation as computation. Specifications of intent in the form of types are preserved and exploited during compilation and linking, alongside the mere computation of a program. This provides lightweight guarantees for compilation, optimization, and linking. Unfortunately, type-preserving compilation typically interferes with important optimizations. In this paper, we study typed closure representation and optimization. We analyze limitations in prior typed closure conversion representations, and the requirements of many important closure optimizations. We design a new typed closure representation in our Flat-Closure Calculus (FCC) that admits all these optimizations, prove type safety and subject reduction of FCC, prove type preservation from an existing closure converted IR to FCC, and implement common closure optimizations for FCC.

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.