My scholarly activity feed.
- 2025
All about Servant
- authors: Harley Eades III
- 2023
Combining Dependency, Grades, and Adjoint Logic
- authors: Peter Hanukaev, Harley Eades III
- doi: 10.1145/3609027.3609408
CrossFit+HCI: Improving the Design of Remote Fitness Coaching Platforms
- authors: Harley Eades III
- pdf: paper.pdf
- 2021
Graded Modal Dependent Type Theory
- authors: Ben Moon, Harley Eades III, Dominic Orchard
- doi: 10.1007/978-3-030-72019-3_17
- 2020
A graded dependent type system with a usage-aware semantics (extended version)
- authors: Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, Stephanie C Weirich
- doi: 10.1145/3434331
- arxiv: 2011.04070
Towards Graded Modal Dependent Types
- authors: Benjamin Moon, Harley Eades III, Dominic Orchard
- link: https://granule-project.github.io/papers/towards-graded-modal-dependent-types.pdf
The Graded Lambek Calculus
- authors: Aubrey Bryant, Harley Eades III
- pdf: abstract.pdf
Grading Adjoint Logic
- authors: Harley Eades III, Dominic Orchard
- arxiv: 2006.08854
Unifying graded and parameterised monads
- authors: Dominic Orchard, Philip Wadler, Harley Eades III
- doi: 10.4204/EPTCS.317.2
On Linear Modalities for Exchange, Weakening, and Contraction
- venue: Workshop on Linear Logic, Mathematics, and Computer Science. Associated with Linear Logic: Interaction, Proofs, and Computation (LL2016)
- slides: /slides
Graded Modal Types
- venue: Seminar Talk, Principles of Programming Group (PoP), Computer Science Department, Carnegie Mellon University
- slides: slides.pdf
- 2019
Quantitative Program Reasoning with Graded Modal Types
- authors: Dominic Orchard, Vilem-Benjamin Liepelt, Harley Eades III
- doi: 10.1145/3341714
- pdf: paper.pdf
My Path from Special Education to Assistant Professor
- authors: Harley Eades III
On the Lambek Calculus with an Exchange Modality
- authors: Jiaming Jiang, Harley Eades III, Valeria de Paiva
- doi: 10.4204/EPTCS.292.4
- 2018
On Linear Logic, Functional Programming, and Attack Trees
- authors: Harley Eades III, Jiaming Jiang, Aubrey Bryant
- doi: 10.1007/978-3-030-15465-3_5
- pdf: paper.pdf
- slides: slides.pdf
On the Lambek Calculus with an Exchange Modality
- authors: Jiaming Jiang, Harley Eades III, Valeria de Paiva
- pdf: paper.pdf
- slides: slides.pdf
Explaining Type Errors
- authors: Brent Yorgey, Richard A. Eisenberg, Harley Eades III
- pdf: abstract.pdf
Dialectica Categories for the Lambek Calculus
- authors: Valeria de Paiva, Harley Eades III
- doi: 10.1007/978-3-319-72056-2_16
- pdf: paper.pdf
- slides: /slides
Advancing PL Based Formal Methods Research and Education
- venue: The Programming Languages and Systems (PLAS) Seminar at University of Kent
- slides: slides.pdf
- 2017
Introducing a New Project on The Combination of Substructural Logics and Dependent Type Theory
- authors: Harley Eades III
- pdf: paper.pdf
Dialectica categories for the Lambek calculus
- authors: Valeria de Paiva, Harley Eades III
Constructive Temporal Logic, Categorically
- authors: Valeria de Paiva, Harley Eades III
- link: http://www.collegepublications.co.uk/downloads/ifcolog00013.pdf
- pdf: paper.pdf
- 2016
Dualized Simple Type Theory
- authors: Harley Eades III, Aaron Stump, Ryan McCleeary
- doi: 10.2168/LMCS-12(3:2)2016
Multiple Conclusion Linear Logic: Cut-elimination and more
- authors: Harley Eades III, Valeria de Paiva
- doi: 10.1007/978-3-319-27683-0_7
- extended: extended.pdf
The Three Perspectives of Computation
- venue: Department of Mathematical Sciences Colloquium Speaker. Georgia Southern University
- slides: /slides
Multiple Conclusion Linear Logic: Cut Elimination and more
- venue: Logical Foundations of Computer Science (LFCS)
- slides: slides.pdf
A New Foundation of Attack Trees in Monoidal Categories
- venue: Computer Science Department Colloquium Speaker. University of Iowa
- slides: /slides
- 2015
Full Intuitionistic Linear Logic (FILL)
- authors: Harley Eades III, Valeria de Paiva
Two-sided Linear Sequent Calculus
- authors: Elaine Pimentel, Harley Eades III
- link: http://proofsystem.github.io/Encyclopedia/
Full Intuitionistic Logic
- authors: Harley Eades III, Valeria de Paiva
- link: http://proofsystem.github.io/Encyclopedia/
Constructive Modal Logic S4 (CS4)
- authors: Harley Eades III, Valeria de Paiva
- link: http://proofsystem.github.io/Encyclopedia/
- 2014
The Semantic Analysis of Advanced Programming Languages
- authors: Harley Eades III
- pdf: thesis.pdf
Hereditary Substitution for the λΔ-Calculus
- venue: Fifth International Workshop on Classical Logic and Computation (CL&C). Affiliated with the joint meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Part of the Vienna Summer of Logic .
- slides: slides.pdf
- 2013
Reconsidering Intuitionistic Duality
- authors: Aaron Stump, Harley Eades III, Ryan McCleeary
- extended: extended-abstract.pdf
- pdf: abstract.pdf
Hereditary Substitution for the λΔ-Calculus
- authors: Harley Eades III, Aaron Stump
- doi: 10.4204/EPTCS.127.4
- slides: slides.pdf
The Categorical Structure of Semi-Bilinear Intuitionistic Logic
- authors: Harley Eades III
- pdf: abstract.pdf
Equational reasoning about programs with general recursion and call-by-value semantics
- authors: Garrin Kimmell, Aaron Stump, Harley Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm SJoberg, Nathan Collins, Ki Yung Ahn
- doi: 10.2201/NiiPi.2013.10.3
On the Categorical Structure of Bi-Intuitionistic Logics
- venue: The University of Iowa Mini-Symposium
- slides: slides.pdf
- 2012
Exploring the Reach of Hereditary Substitution
- authors: Harley Eades III, Aaron Stump
- pdf: paper.pdf
- slides: slides.pdf
LFSC for SMT Proofs: Work in Progress
- authors: Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang
- link: http://ceur-ws.org/Vol-878/paper1.pdf
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
- authors: Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich
- doi: 10.4204/EPTCS.76.9
Equational reasoning about programs with general recursion and call-by-value semantics
- authors: Garrin Kimmell, Aaron Stump, Harley Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjoberg, Nathan Collins, Ki Yung Ahn
Hereditary Substitution for the λΔ-Calculus
- venue: Fourth International Workshop on Classical Logic and Computation. Affiliated with ICALP
- slides: slides.pdf
Hereditary Substitution for Classical Natural Deduction
- venue: Trellys Meeing. Held at the University of Pennsylvania
- slides: slides.pdf
Exploring the Reach of Hereditary Substitution
- venue: University of Pennsylvania PL Club
- slides: slides.pdf
- 2011
Separation from Proof and Program
- venue: Midwest Verification Day
- slides: slides.pdf
- 2010
Hereditary Substitution for Stratified System F
- authors: Harley Eades III, Aaron Stump
- pdf: paper.pdf
- 2009
Zero-Divisors and Their Graph Languages
- authors: Harley Eades III
- pdf: paper.pdf