Publications

Papers in Proceedings 13

Peter Hanukaev, Harley Eades III. Combining Dependency, Grades, and Adjoint Logic. TyDe 2023: Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development. doi: 10.1145/3609027.3609408
Ben Moon, Harley Eades III, Dominic Orchard. Graded Modal Dependent Type Theory. In the Proceedings of the 30th European Symposium on Programming (ESOP2021), pp 462-490.. doi: 10.1007/978-3-030-72019-3_17 [PDF]
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, Stephanie C Weirich. A graded dependent type system with a usage-aware semantics (extended version). Proc. ACM Program. Lang. 5, POPL, Article 50 (January 2021), 32 pages.. doi: 10.1145/3434331 [PDF]
Dominic Orchard, Philip Wadler, Harley Eades III. Unifying graded and parameterised monads. In the Proceedings of the Eighth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2020, Dublin, Ireland, 25th April 2020. Electronic Proceedings in Theoretical Computer Science (EPTC) 317, pages 18--38.. doi: 10.4204/EPTCS.317.2 [PDF]
Jiaming Jiang, Harley Eades III, Valeria de Paiva. On the Lambek Calculus with an Exchange Modality. In the Proceedings of The Joint Workshop on Linearity & TLLA, co-located with Third International Conference on Formal Structures for Computation and Deduction (FCSD) in conjunction with the Federated Logic Conference. Electronic Proceedings in Theoretical Computer Science (EPTC) 292, pages 43–89. doi: 10.4204/EPTCS.292.4
Harley Eades III, Jiaming Jiang, Aubrey Bryant. On Linear Logic, Functional Programming, and Attack Trees. In: Cybenko G., Pym D., Fila B. (eds) Graphical Models for Security. GraMSec 2018. Lecture Notes in Computer Science, vol 11086. Springer, Cham.. doi: 10.1007/978-3-030-15465-3_5 [PDF]
Valeria de Paiva, Harley Eades III. Dialectica Categories for the Lambek Calculus. In: Artemov S., Nerode A. (eds) Logical Foundations of Computer Science. LFCS 2018. Lecture Notes in Computer Science, vol 10703. Springer, Cham. doi: 10.1007/978-3-319-72056-2_16 [PDF]
Harley Eades III, Valeria de Paiva. Multiple Conclusion Linear Logic: Cut-elimination and more. Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS 2016). doi: 10.1007/978-3-319-27683-0_7 [PDF (with proofs)]
Harley Eades III, Aaron Stump. Hereditary Substitution for the λΔ-Calculus. Proceedings of the First Workshop on Control Operators and their Semantics (COS 2013). [Slides] doi: 10.4204/EPTCS.127.4
Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang. LFSC for SMT Proofs: Work in Progress. Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving (PXTP 2012). [PDF]
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich. Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems. Proceedings Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012). doi: 10.4204/EPTCS.76.9
Garrin Kimmell, Aaron Stump, Harley Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjoberg, Nathan Collins, Ki Yung Ahn. Equational reasoning about programs with general recursion and call-by-value semantics. doi: 10.1145/2103776.2103780
Harley Eades III, Aaron Stump. Hereditary Substitution for Stratified System F. Workshop on Proof-Search in Type Theories (PSTT). [PDF]

Journal Papers 5

Dominic Orchard, Vilem-Benjamin Liepelt, Harley Eades III. Quantitative Program Reasoning with Graded Modal Types. Proceedings of the ACM on Programming Languages (PACMPL), 18 August 2019. Volume 3, Issue ICFP, 30 pages. doi: 10.1145/3341714 [PDF]
Valeria de Paiva, Harley Eades III. Constructive Temporal Logic, Categorically. IFCoLog Journal of Logic and its Applications, 01 February 2017. Volume 4, Number 4, Special Issue Dedicated to the Memory of Grigori Mints. [PDF]
Harley Eades III, Aaron Stump, Ryan McCleeary. Dualized Simple Type Theory. Logical Methods in Computer Science, 15 August 2016. Volume 12, Issue 3. doi: 10.2168/LMCS-12(3:2)2016
Garrin Kimmell, Aaron Stump, Harley Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm SJoberg, Nathan Collins, Ki Yung Ahn. Equational reasoning about programs with general recursion and call-by-value semantics. Special Issue of Progress in Informatics on Advanced Programming Techniques for Construction of Robust, General and Evolutionary Programs, number 10. Pages 19-46. 01 March 2013. The journal version of the PLPV12 paper. doi: 10.2201/NiiPi.2013.10.3
Harley Eades III. Zero-Divisors and Their Graph Languages. Rose-Hulman Undergraduate Mathematics Journal, volume 10. number 2. 04 January 2009. [PDF]

Abstracts 10

Harley Eades III. CrossFit+HCI: Improving the Design of Remote Fitness Coaching Platforms. Accepted for presentation at The Workgroup on Interactive Systems in Healthcare (WISH) workshop 2023 colocated with CHI 2023.. 24 February 2023. [PDF]
Benjamin Moon, Harley Eades III, Dominic Orchard. Towards Graded Modal Dependent Types (extended abstract). The workshop on Type-Driven Development colocated with the 25th ACM SIGPLAN International Conference on Functional Programming (ICFP).. 23 August 2020. [PDF]
Harley Eades III, Dominic Orchard. Grading Adjoint Logic. Abstract (2 pages): 2020 Joint Workshop on Linearity & TLLA: The 6th Workshop on Linearity and the 4th Workshop on Trends in Linear Logic and Applications. 29 June 2020. [PDF]
Aubrey Bryant, Harley Eades III. The Graded Lambek Calculus. Extended Abstract (8 pages): 2020 Joint Workshop on Linearity & TLLA: The 6th Workshop on Linearity and the 4th Workshop on Trends in Linear Logic and Applications. 29 June 2020. [PDF]
Jiaming Jiang, Harley Eades III, Valeria de Paiva. On the Lambek Calculus with an Exchange Modality. Extended Abstract (8 pages): 2018 Joint Workshop on Linearity & TLLA: The 5th Workshop on Linearity and the 2nd Workshop on Trends in Linear Logic and Applications. 07 July 2018. [PDF]
Brent Yorgey, Richard A. Eisenberg, Harley Eades III. Explaining Type Errors. Off the Beaten Track (OBT 2018). Associated with The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018). 13 January 2018. [PDF]
Harley Eades III. Introducing a New Project on The Combination of Substructural Logics and Dependent Type Theory. International Workshop on Trends in Linear Logic and Applications (TLLA) affiliated with the Second International Conference on Formal Structures for Computation and Deduction (FSCD). 31 July 2017. [PDF]
Valeria de Paiva, Harley Eades III. Dialectica categories for the Lambek calculus. Association for Symbolic Logic (ASL) Spring Meeting jointly held with the Annual Meeting of the Pacific Division of the American Philosophical Association. 15 April 2017.
Harley Eades III, Jiaming Jiang. On Linear Modalities for Exchange, Weakening, and Contraction. Workshop on Linear Logic, Mathematics, and Computer Science. Associated with Linear Logic: Interaction, Proofs, and Computation (LL2016). 09 November 2016. [PDF]
Aaron Stump, Harley Eades III, Ryan McCleeary. Extended Abstract: Reconsidering Intuitionistic Duality. Control Operators and their Semantics (COS 2013). 04 September 2013. [PDF] [PDF (with proofs)]

Posters 1

Harley Eades III, Valeria de Paiva. Full Intuitionistic Linear Logic (FILL). Presented as a Poster at the 25th jubilee edition of the International Conference on Automated Deduction (CADE). Entry in Encyclopedia of Proof Systems: http://proofsystem.github.io/Encyclopedia/. 2015.

Unpublished 11

Harley Eades III, Gianluigi Bellin. A Cointuitionistic Adjoint Logic. Under review at Logical Methods in Computer Science (LMCS). 2017. [PDF]
Harley Eades III, Valeria de Paiva. Lambek Calculus. Entry in Encyclopedia of Proof Systems: http://proofsystem.github.io/Encyclopedia/. 2016.
Harley Eades III. Proposing a New Foundation of Attack Trees in Monoidal Categories. Updated: March 30. 2016. [PDF]
Harley Eades III, Valeria de Paiva. Full Intuitionistic Logic. Entry in Encyclopedia of Proof Systems: http://proofsystem.github.io/Encyclopedia/. 2015.
Harley Eades III, Valeria de Paiva. Constructive Modal Logic S4 (CS4). Entry in Encyclopedia of Proof Systems: http://proofsystem.github.io/Encyclopedia/. 2015.
Elaine Pimentel, Harley Eades III. Two-sided Linear Sequent Calculus. Entry in Encyclopedia of Proof Systems: http://proofsystem.github.io/Encyclopedia/. 2015.
Harley Eades III. The Semantic Analysis of Advanced Programming Languages. Ph.D. Thesis: The Unversity of Iowa. 2014. [PDF]
Harley Eades III. Extended Abstract: The Categorical Structure of Semi-Bilinear Intuitionistic Logic. Presented at the Midwest Verification Day. 2013. [PDF]
Harley Eades III. Type Theory and Applications. Ph.D. Comprehensive Exam. 2012. [PDF]
Harley Eades III. Using the Hereditary Substitution Function in Normalization Proofs. Ph.D. Qualifying Exam. 2011. [Slides] [PDF]
Harley Eades III, Aaron Stump. Exploring the Reach of Hereditary Substitution. Presented at TYPES 2012. [Slides] [PDF]