Joshua Grosso[1]
Email: jtgrosso@cs.cmu.edu
Twitter: @JoshuaGrosso
GitHub: jgrosso
LinkedIn: linkedin.com/in/JoshuaGrosso
About Me
I'm Joshua Grosso, a first-year Ph.D. student at the Computer Science Department in CMU's School of Computer Science. My focus is on programming languages, type theory, and interactive theorem proving, and I am advised by Karl Crary. I earned my undergraduate degree from Caltech (B.S. in Computer Science, '23).
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 experiences with formal verification have shown me there’s still a long way to go before we can bridge the gap between theory and practice. 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. homotopy type theory).
I'm 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.
I'm also very interested in linguistics, especially phonetics, and pure mathematics in general.
Projects
A
EL
2017–present
EL
The Axel programming language: Haskell's semantics, plus Lisp's macros. Axel adds Clojure[2]-like syntax and macro capabilities to Haskell, while remaining compatible with existing Haskell code.
Theoretical Pearl: α-equivalence is easy2021–present
I formalized Functional Pearls: α-conversion is easy (Altenkirch, 2002, unpublished), which presents a simple algorithm for calculating α-equivalence, using the Coq proof assistant. During my formalization, I discovered and repaired several errors in the definitions, propositions, and proofs. I am currently working with Dr. Altenkirch to update the original manuscript and prepare it for submission (we plan to submit jointly to the Journal of Functional Programming).
Formal verification of Types and Programming Languages2020–2021
Under the supervision of my research mentor, Michael Vanier, I formalized existing programming language research using the Coq proof assistant. Our main focus was on the material in Types and Programming Languages (Pierce, 2002), picking up where Programming Language Foundations (Pierce et al.) leaves off.