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