Joshua Grosso
Email: jtgrosso@cmu.edu
Twitter: @JoshuaGrosso
GitHub: jgrosso
LinkedIn: linkedin.com/in/JoshuaGrosso
About Me
I'm Joshua Grosso,[1] a third-year Ph.D. student in the Computer Science Department of 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 completed my undergraduate degree at 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 (e.g. language ergonomics) or the theoretical side (e.g. computational 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.
Projects
A
EL
2017–present
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.
Personal
-
I'm a Christian (perhaps most centrally, I believe in the Trinity[3] as well as "justification by faith alone", i.e. sola fide). This is the core of my identity, and I hope my life reflects it in some small way. I'm always happy to talk about God!
For God so loved the world that he gave his one and only Son, that whoever believes in him shall not perish but have eternal life. For God did not send his Son into the world to condemn the world, but to save the world through him. Whoever believes in him is not condemned, but whoever does not believe stands condemned already because they have not believed in the name of God’s one and only Son.
John 3:16–18 (NIV)Love is patient, love is kind. It does not envy, it does not boast, it is not proud. It does not dishonor others, it is not self-seeking, it is not easily angered, it keeps no record of wrongs. Love does not delight in evil but rejoices with the truth. It always protects, always trusts, always hopes, always perseveres.
1 Corinthians 13:4–7 (NIV)But [God] said to me, “My grace is sufficient for you, for my power is made perfect in weakness.” Therefore I will boast all the more gladly about my weaknesses, so that Christ’s power may rest on me.
2 Corinthians 12:9 (NIV) - I'm interested in linguistics, especially phonetics and phonology. (日本語が少しできますが、まだまだなんです｡）