Harrison Grodin


I’m a Ph.D. student in the Computer Science Department at Carnegie Mellon University, advised by Robert Harper. My primary interests are programming languages, type theory, category theory, and logic.

I completed my undergraduate degree at Carnegie Mellon University in the School of Computer Science, with a major in Computer Science and an additional major in Logic and Computation, in the spring of 2022.


Jan 2024   📘 publish Decalf: A Directed, Effectful Cost-Aware Logical Framework at POPL 2024
Jan 2024   👥 attend POPL 2024 in London, UK
Dec 2023   👥 attend Jane Street Programming Languages Colloquium in New York City, NY
Sep 2023   📝 publish a preprint about verifying joinable red-black trees in calf
Sep 2023   📘 publish Amortized Analysis via Coinduction at CALCO 2023

selected publications

  1. Decalf: A Directed, Effectful Cost-Aware Logical Framework
    Harrison GrodinRobert Harper, Yue Niu, and Jonathan Sterling
  2. Amortized Analysis via Coinduction
    Harrison Grodin and Robert Harper
    In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023), Sep 2023
  3. A Cost-Aware Logical Framework
    Yue Niu, Jonathan SterlingHarrison Grodin, and Robert Harper
    Proceedings of the ACM on Programming Languages, Jan 2022