Jared Roesch

About

You have stumbled upon the personal website of Jared Roesch.

I’m a fourth year PhD student in the PLSE group at the University of Washington. I am advised by Zach Tatlock and frequently collaborate with Leonardo de Moura. I am interested in designing new tools for building, optimizing and reasoning about critical software.

Projects

My work is currently focused around the TVM stack.

My main focus designing a new intermediate representation for deep learning frameworks with Tianqi Chen with the help of many others from SAMPL. Our goal is to tackle many of the challenges presented by current deep learning frameworks and compiler.

This new IR is named Relay and is now part of the TVM Project. Relay is under heavy development, but you can find initial details in the RFC we drafted.

Past Projects

EBPF

One focuses on a design for constructing verified compilers which execute in adversarial environments, in particular one for eBPF in the Linux kernel.

Lean

I am also working on various pieces of the Lean programming language and theorem prover, including native compilation, sledgehammer style tactics, and various development tools including editor modes.

Everest

I also worked on the F* programming language, which has been co-designed with miTLS as part of the larger Everest Expedition.

In particular I designed an experimental Lean backend for F* verfication conditions, and have been contributing to the design and implementation of low level programming libraries in F* and efficient compilation of F* to C.

Rust

When time permits I attempt to contribute to Rust.

Personal

I was previously at the University of California Santa Barbara where I was a member of the PL Lab and the ArchLab.

In my professional life I worked at the now defunct Zentopy on a cloud file system, at Invoca on distributed systems and infrastructure, and Mozilla Research on the Rust programing language.

In my personal life I grew up in sunny California and have spent most of my life there. I enjoy cooking, listening, writing and playing music, reading, type theory, hacking, coffee, and sleep (when I can).

I am excited about working with motivated undergraduates from many backgrounds and interests. Currently my interests are around compiler hacking, programming languages for machine learning, machine learning for programming language, verification, program analysis, type theory, and more. I am always excited to talk to undergraduate students about research, and the research process, even if just for a cup of coffee. Feel free to drop me a line!