Joseph Rotella

I am an incoming Ph.D. student in the Programming Research Laboratory at Northeastern University. 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. I spent many semesters as a TA for courses on interactive theorem proving, discrete math, and (at Carnegie Mellon) functional programming.

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