Equational reasoning about programs with general recursion and call-by-value semantics. - Garrin Kimmell; Aaron Stump; Harley D. Eades III; Peng Fu 001; Tim Sheard; Stephanie Weirich; Chris Casinghino; Vilhelm Sjöberg; Nathan Collins; Ki Yung Ahn (PLPV, 2012)

LFSC for SMT Proofs: Work in Progress. - Aaron Stump; Andrew Reynolds 001; Cesare Tinelli; Austin Laugesen; Harley Eades III; Corey Oliver; Ruoyu Zhang (PxTP, 2012)

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems - Vilhelm Sjöberg; Chris Casinghino; Ki Yung Ahn; Nathan Collins; Harley D. Eades III; Peng Fu 001; Garrin Kimmell; Tim Sheard; Aaron Stump; Stephanie Weirich (MSFP, 2012)

Hereditary Substitution for the λΔ-Calculus. - Harley Eades III; Aaron Stump (COS, 2013)

Dualized Simple Type Theory. - Harley Eades III; Aaron Stump; Ryan McCleeary (Log. Methods Comput. Sci., 2016)

A Cointuitionistic Adjoint Logic. - Harley Eades III; Gianluigi Bellin (CoRR, 2017)

Constructive Temporal Logic, Categorically. - Valeria de Paiva; Harley Eades III (FLAP, 2017)

On Linear Logic, Functional Programming, and Attack Trees. - Harley Eades III; Jiaming Jiang; Aubrey Bryant (GraMSec@FLoC, 2018)

Dialectica Categories for the Lambek Calculus. - Valeria de Paiva; Harley Eades III (LFCS, 2018)

An Intuitionistic Linear Logical Semantics of SAND Attack Trees. - Harley Eades III (CoRR, 2018)

On the Lambek Calculus with an Exchange Modality. - Jiaming Jiang; Harley Eades III; Valeria de Paiva (Linearity-TLLA@FLoC, 2018)

Quantitative program reasoning with graded modal types. - Dominic Orchard; Vilem-Benjamin Liepelt; Harley Eades III (Proc. ACM Program. Lang., 2019)

Unifying graded and parameterised monads. - Dominic Orchard; Philip Wadler; Harley Eades III (MSFP@ETAPS, 2020)

Grading Adjoint Logic. - Harley Eades III; Dominic Orchard (CoRR, 2020)

A graded dependent type system with a usage-aware semantics (extended version). - Pritam Choudhury; Harley Eades III; Richard A. Eisenberg; Stephanie C. Weirich (CoRR, 2020)

Multiple conclusion linear logic: cut elimination and more. - Harley Eades III; Valeria de Paiva (J. Log. Comput., 2020)

Graded Modal Dependent Type Theory. - Benjamin Moon; Harley Eades III; Dominic Orchard (ESOP, 2021)

A graded dependent type system with a usage-aware semantics. - Pritam Choudhury; Harley Eades III; Richard A. Eisenberg; Stephanie Weirich (Proc. ACM Program. Lang., 2021)

A Dependent Dependency Calculus. - Pritam Choudhury; Harley Eades III; Stephanie Weirich (ESOP, 2022)

A Dependent Dependency Calculus (Extended Version). - Pritam Choudhury; Harley Eades III; Stephanie Weirich (CoRR, 2022)

Combining Dependency, Grades, and Adjoint Logic. - Peter Hanukaev; Harley Eades III (TyDe@ICFP, 2023)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models. - Victoria Vollmer; Danielle Marshall 001; Harley Eades III; Dominic Orchard (CSL, 2025)