Harrison Grodin

prof_pic.jpg

I’m a third-year Ph.D. student in the Principles of Programming group in the Computer Science Department at Carnegie Mellon University, advised by Robert Harper. My research is focused on programming language semantics, drawing inspiration from ideas in type theory and category theory.

Currently, I am developing Calf, a dependent type theory for verifying the cost and behavior of algorithms and data structures. Central themes in this project are effects, phase distinctions, exact and inexact bounds, and parallelism.

news

Dec 2024   🗣️ present at the Topos Institute Berkeley Seminar in Berkeley, CA
Nov 2024   📘 publish Amortized Analysis via Coalgebra in the Proceedings of MFPS XL
Jun 2024   🗣️ present at MFPS 2024 in Oxford, UK
May 2024   🧑‍🏫 teach Principles of Functional Programming summer semester
Apr 2024   🏆 receive an Honorable Mention for the Jane Street Graduate Research Fellowship

selected publications

  1. Amortized Analysis via Coalgebra
    Harrison Grodin, and Robert Harper
    Mathematical Foundations of Programming Semantics, Jun 2024
  2. Decalf: A Directed, Effectful Cost-Aware Logical Framework
    Harrison GrodinYue NiuJonathan Sterling, and Robert Harper
    Proceedings of the ACM on Programming Languages, Jan 2024
  3. A Cost-Aware Logical Framework
    Yue NiuJonathan SterlingHarrison Grodin, and Robert Harper
    Proceedings of the ACM on Programming Languages, Jan 2022