8 citations · 12 across the 7 of their papers we have counts for
9 papers
A Dependent Dependency Calculus (Extended Version)
Pritam Choudhury, Harley Eades, Stephanie Weirich
Over twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since the…
A graded dependent type system with a usage-aware semantics (extended version)
Pritam Choudhury, Harley Eades, Richard A. Eisenberg +1
Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type sy…
Graded Modal Dependent Type Theory
Benjamin Moon, Harley Eades, Dominic Orchard
Graded type theories are an emerging paradigm for augmenting the reasoning power of types with parameterizable, fine-grained analyses of program properties. There have been many su…
Grading Adjoint Logic
Harley Eades, Dominic Orchard
We introduce a new logic that combines Adjoint Logic with Graded Necessity Modalities. This results in a very expressive system capable of controlling when and how structural rules…
Unifying graded and parameterised monads
Dominic Orchard, Philip Wadler, Harley Eades
Monads are a useful tool for structuring effectful features of computation such as state, non-determinism, and continuations. In the last decade, several generalisations of monads…
On the Lambek Calculus with an Exchange Modality
Jiaming Jiang, Harley Eades, Valeria de Paiva
In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton's Linear/Non-Linear Logic by removing…