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 | 95 | 2019 |
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 | 37 | 2021 |
Graded modal dependent type theory B Moon, H Eades III, D Orchard European Symposium on Programming, 462-490, 2021 | 34 | 2021 |
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 | 34 | 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 | 33 | 2012 |
Unifying graded and parameterised monads D Orchard, P Wadler, H Eades III arXiv preprint arXiv:2001.10274, 2020 | 16 | 2020 |
Hereditary substitution for stratified system f H Eades, A Stump International Workshop on Proof-Search in Type Theories, PSTT 10, 2010 | 13 | 2010 |
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 |
A Dependent Dependency Calculus P Choudhury, H Eades III, S Weirich European Symposium on Programming, 403-430, 2022 | 7 | 2022 |
On the lambek calculus with an exchange modality J Jiang, H Eades III, V de Paiva arXiv preprint arXiv:1904.06847, 2019 | 7 | 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 |
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 | 5 | 2019 |
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 |
Combining dependency, grades, and adjoint logic P Hanukaev, H Eades III Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven …, 2023 | 4 | 2023 |
The semantic analysis of advanced programming languages HD Eades III The University of Iowa, 2014 | 4 | 2014 |
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 | 2 | 2020 |
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 |