Structures for structural recursion. - Paul Downen; Philip Johnson-Freyd; Zena M. Ariola (ICFP, 2015)

First Class Call Stacks: Exploring Head Reduction. - Philip Johnson-Freyd; Paul Downen; Zena M. Ariola (WoC, 2015)

Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System. - Philip Johnson-Freyd; Geoffrey C. Hulette; Zena M. Ariola (FMICS-AVoCS, 2016)

Call-by-name extensionality and confluence. - Philip Johnson-Freyd; Paul Downen; Zena M. Ariola (J. Funct. Program., 2017)

Uniform Strong Normalization for Multi-discipline Calculi. - Paul Downen; Philip Johnson-Freyd; Zena M. Ariola (WRLA@ETAPS, 2018)

Topos Semantics for a Higher-Order Temporal Logic of Actions. - Philip Johnson-Freyd; Jon Aytac; Geoffrey C. Hulette (ACT, 2019)

Abstracting models of strong normalization for classical calculi. - Paul Downen; Philip Johnson-Freyd; Zena M. Ariola (J. Log. Algebraic Methods Program., 2020)

A Nominal Approach to Probabilistic Separation Logic. - John M. Li; Jon Aytac; Philip Johnson-Freyd; Amal Ahmed 001; Steven Holtzen (LICS, 2024)

A Formalization of Core Why3 in Coq. - Joshua M. Cohen; Philip Johnson-Freyd (Proc. ACM Program. Lang., 2024)