Joseph Rotella

I am a Ph.D. student in the Programming Research Laboratory at Northeastern University, where I am advised by Chris Martens. Previously, I was a Research Software Engineer at the Lean FRO, where I helped develop the Lean programming language and theorem prover. Before that, I worked on the AILean project as an intern at Amazon Web Services.

I received my Sc.B. in Mathematics and Computer Science from Brown University, where I wrote my honors thesis, advised by Robert Y. Lewis, on verified tabular programming in Lean. (See also my talk at Lean Together 2025.) I spent many semesters as a TA for courses on interactive theorem proving, discrete math, and (at Carnegie Mellon) functional programming.

I can be reached by concatenating my first and last initials, the usual separator, and the domain of this website. My code can be found on GitHub and my professional credentials on LinkedIn.