Joseph Rotella

I am a recent graduate of Brown University, where I received my Sc.B. in Mathematics and Computer Science. My interests center on programming languages and logic; I've spent much of the past four years working with the Lean theorem prover and programming language. I wrote my honors thesis, advised by Robert Y. Lewis, on verified tabular programming in Lean. In the summer of 2024, I was an intern at Amazon Web Services, where I worked on the AILean project. I also 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.