Papers

Pattern Matching in AI Compilers and its Formalization
Joseph W. Cutler, Alex Collins, Bin Fan, Mahesh Ravishankar, Vinod Grover
CGO '25
Stream Types
Joseph W. Cutler, Christopher Watson, Emeka Nkurumeh, Phillip Hilliard, Harrison Goldstein, Caleb Stanford, Benjamin C. Pierce
PLDI '24 [Extended Version] [Talk Video] [Implementation]
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization
Cutler*, Disselkoen, Eline, He, Headley, Hicks, Hietala, Ioannidis, Kastner, Mamat, McAdams, McCutcheon, Rungta, Torlak, Wells
OOPSLA '24
Property-Based Testing in Practice (Distinguished Paper Award 🏆)
Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, Andrew Head
ICSE '24
Denotational Cost Semantics for Amortized Analysis.
Joseph W. Cutler, Daniel R. Licata, Norman Danner.
ICFP '20. [Extended Version] [Slides][Talk Video]

* Authors listed alphabetically

Workshop Papers & Drafts

Improving the Stability of Type Soundness Proofs in Dafny
Joseph W. Cutler, Michael W. Hicks, Emina Torlak
Dafny Workshop '24 [Talk Video]
Some Problems with Properties: A Study on Property-Based Testing in Industry
Harrison Goldstein, Joseph W. Cutler, Adam Stein, Benjamin C. Pierce, Andrew Head
HATRA Workshop '22
Holey Generators!
Joseph W. Cutler, Harrison Goldstein, Koen Claessen, John Hughes, Benjamin C. Pierce
Unpublished Draft, 2022

Langauges with Potential: Types & Recurrences for Formal Amortized Analysis
Joseph W. Cutler
Wesleyan University Undergraduate Thesis. Awarded High Honors.
Transducers are Causal Functions. Joseph W. Cutler
Course Project, CIS 6700, Fall 2022
Automatic Detection of Hybrid Human-Machine Text Boundaries. Joseph W. Cutler, Liam Dugan, Shreya Havaldar, Adam Stein.
Course Project, CIS 520, Fall 2021
Conferences after COVID: An Early-Career Perspective. Joseph W. Cutler, Harry Goldstein, Andrew K. Hirsch, Jaemin Hong, Chandrakana Nandi.
SIGPLAN Blog "PL Perspectives": March 25, 2021.

I've been super lucky to get to work with and mentor some wonderful undergrads at Penn, some as part of the awesome REPL program.

Emeka Nkurumeh (REPL, Caltech c/o 2025): Built the first version of the Delta typechecker.
Will Sturgeon (c/o 2024): Worked on Coq proofs of Stream Types metatheory.
Tanner Duve (c/o 2025): Learned about proof theory.

TA for Penn CIS 5520: Advanced Programming (Fall 2022)
TA for Wesleyan COMP 360: Applied Logic & Logic Programming (Fall 2020)
TA for Wesleyan COMP 323: Programming Language Implementation (Spring 2020)
TA for Wesleyan COMP 212: Computer Science II. (S/F 2018, S 2019, S/F 2020, S 2021)
TA for Wesleyan COMP 112: Introduction To Programming. (Summer 2018)
TA for Wesleyan MATH 261: Abstract Algebra (Fall 2020)
TA for Wesleyan MATH 223: Linear Algebra. (Fall 2019)

Getting Fusion in Order (Programming Languages @ Harvard , November 1, 2024)
Delta: Ordered Types for Stream Processing (Programming Systems Group @ Uber, August 14, 2024)
Delta: Ordered Types for Stream Processing (PLSE Lunch @ UW CSE, July 9, 2024)
Delta: Ordered Types for Stream Processing (LSD Seminar @ UCSC, Feb 2, 2024)
Delta: Ordered Types for Stream Processing (Jane Street Programming Languages Colloqium, December 15, 2023)
Essence of Structured Streaming Computation (Chalmers Stream Processing Seminar, October 9, 2023)
Essence of Structured Streaming Computation (ACSYS Seminar @ NYU, October 5, 2023)
Essence of Structured Streaming Computation (ROSE Seminar @ Yale, October 4, 2023)
Bunched and Ordered Types for Stream Processing (NJPLS @ UMD, October 21, 2022)

Thanks to Joomy Korkut for letting me steal his website!

Last updated: