Joseph Rotella

I am a Ph.D. student in the Programming Research Laboratory at Northeastern University, where I am advised by Chris Martens. I enjoy thinking about dependent types, logic, and proof assistants.

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 at rotella.jo at my university’s domain.

Papers

• Synthetic Theorem Generation in Lean
  Joseph Rotella, Zhizhen Qin, Aidan Z.H. Yang, Brando Miranda, Mohamed El Amine Seddik, Jingwei Zuo, Hakim Hacid, Leonardo de Moura, Soonho Kong*, Shi Hu*. Preprint, 2025.
  Local copy | OpenReview

• Dependently Typed Tables
  Joseph Rotella. Bachelor’s thesis, Brown University, 2024.

  Local copy | Brown CS archive

Talks

• Programming with Dependently Typed Tables in Lean.
  Lean Together, 2025.

  Recording | Slides