Joshua Grosso

Twitter: @JoshuaGrosso
GitHub: jgrosso

About Me

I'm Joshua Grosso, an undergraduate senior at Caltech majoring in Computer Science.
My primary interests are in formal verification and programming language theory; my undergraduate research project (see below) is in this area.
I was a software developer for three years before Caltech (most recently on the GitKraken team at Axosoft); I loved it, but it left me with a sense of unease for the ad-hoc, bug-ridden state of the modern software ecosystem. On the other hand, my brief experiences with Coq have shown me there’s still a long way to go before we can bridge the gap. My hope is to contribute somehow to that effort, whether on the practical side (proof repair, language ergonomics, etc.) or the theoretical side (e.g. HoTT).
Although my current focus is on theoretical computer science, I'm still passionate about software development and improving how we think about and design software systems. In particular, I believe functional programming has great potential, so I'm a big fan of Haskell and related languages.


Formal verification of programming language research (2020-present)

Under the supervision of my research mentor, Michael Vanier, I am formalizing existing programming language research using the Coq proof assistant. Our main focus is on the material in Types and Programming Languages (Pierce, 2002), picking up where Programming Language Foundations (Pierce et al.) leaves off. I'm currently taking a detour to formalize Functional Pearls: ɑ-equivalence is easy (Altenkirch, 2002). The repository is located at

Axel (2017-present)

The Axel programming language: Haskell's semantics, plus Lisp's macros. Axel adds Clojure–like syntax and macro capabilities to Haskell, while remaining compatible with existing Haskell code.