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 third 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.


I am working on a couple active projects.


My main focus designing a new intermediate representation for deep learning frameworks with Tianqi Chen. This IR is intended to be the future of NNVM.


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 interested in working with motivated undergraduates who are interested in compiler hacking, verification, program analysis, type theory, and more. I am always excited to hear from students who are interested in doing research, feel free to email me.

© Jared Roesch 2017