| Quantitative program reasoning with graded modal types D Orchard, VB Liepelt, H Eades III Proceedings of the ACM on Programming Languages 3 (ICFP), 1-30, 2019 | 86 | 2019 |
| Irrelevance, heterogeneous equality, and call-by-value dependent type systems V Sjöberg, C Casinghino, KY Ahn, N Collins, HD Eades III, P Fu, ... arXiv preprint arXiv:1202.2923, 2012 | 31 | 2012 |
| Equational reasoning about programs with general recursion and call-by-value semantics G Kimmell, A Stump, HD Eades III, P Fu, T Sheard, S Weirich, ... Proceedings of the sixth workshop on Programming languages meets program …, 2012 | 31 | 2012 |
| A graded dependent type system with a usage-aware semantics P Choudhury, H Eades III, RA Eisenberg, S Weirich Proceedings of the ACM on Programming Languages 5 (POPL), 1-32, 2021 | 29 | 2021 |
| Graded modal dependent type theory B Moon, H Eades III, D Orchard Programming Languages and Systems 12648, 462, 2021 | 25 | 2021 |
| Hereditary substitution for stratified system f H Eades, A Stump International Workshop on Proof-Search in Type Theories, PSTT 10, 2010 | 15 | 2010 |
| Unifying graded and parameterised monads D Orchard, P Wadler, H Eades III arXiv preprint arXiv:2001.10274, 2020 | 14 | 2020 |
| Dialectica categories for the Lambek calculus V de Paiva, H Eades III International Symposium on Logical Foundations of Computer Science, 256-272, 2017 | 10 | 2017 |
| On the lambek calculus with an exchange modality J Jiang, H Eades III, V de Paiva arXiv preprint arXiv:1904.06847, 2019 | 9 | 2019 |
| Multiple conclusion linear logic: Cut elimination and more H Eades, V de Paiva Logical Foundations of Computer Science: International Symposium, LFCS 2016 …, 2016 | 7 | 2016 |
| LFSC for SMT Proofs: Work in Progress. A Stump, A Reynolds, C Tinelli, A Laugesen, H Eades III, C Oliver, ... PxTP, 21-27, 2012 | 5 | 2012 |
| The preliminary design of the Trellys core language C Casinghino, HD Eades III, G Kimmell, V Sjöberg, T Sheard, A Stump, ... Talk and discussion session at PLPV, 2011 | 5 | 2011 |
| A Dependent Dependency Calculus P Choudhury, H Eades III, S Weirich European Symposium on Programming, 403-430, 2022 | 4 | 2022 |
| On linear logic, functional programming, and attack trees H Eades III, J Jiang, A Bryant Graphical Models for Security: 5th International Workshop, GraMSec 2018 …, 2019 | 4 | 2019 |
| The semantic analysis of advanced programming languages HD Eades III The University of Iowa, 2014 | 4 | 2014 |
| Multiple conclusion linear logic: cut elimination and more H Eades III, V De Paiva Journal of Logic and Computation 30 (1), 157-174, 2020 | 2 | 2020 |
| Dualized simple type theory H Eades III, A Stump, R McCleeary Logical Methods in Computer Science 12, 2017 | 2 | 2017 |
| Hereditary Substitution for the\lambda\Delta-Calculus H Eades, A Stump arXiv preprint arXiv:1309.1256, 2013 | 2 | 2013 |
| Type Theory and Applications H Eades URL: https://metatheorem. org/includes/pubs/comp. pdf, 2012 | 2 | 2012 |
| A graded dependent type system with a usage-aware semantics (extended version) P Choudhury, H Eades III, RA Eisenberg, SC Weirich arXiv preprint arXiv:2011.04070, 2020 | 1 | 2020 |
Aaron StumpProfessor of Computer Science, The University of IowaVerified email at uiowa.edu
