Jared Roesch

Computer Science PhD Student
University of Washington
Office: CSE 410
Lab: CSE 407


April 2018: Our paper An Architecture for Analysis was chosen as an IEEE Micro "Top Pick".
October 13 2017: I am returning to University Washington to resume my studies.
July 17 2017: I will be returning to Microsoft an an intern working on Lean and F*, with Nikhil Swamy and Leo De Moura.
June 19 2017: Our paper on Lean's tactic framework was accepted to ICFP '17
March 20 2017: I will be joining Microsoft Research's RiSE group as an intern working on Lean and F*, with Tahina Ramananandro and Leo De Moura.
Jan 16 2017: Leo, Gabriel, Sebastian and I gave a tutorial on Lean at POPL 2017 in Paris.
Oct 23 2016: Luke will present a poster on our work on a secure eBPF compiler at OSDI 2016!

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.


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


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


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.


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.


When time permits I attempt to contribute to Rust.


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!

© Jared Roesch 2018