17 citations · 42 across the 15 of their papers we have counts for
15 papers
A unification of graded and substructural logics
Peter Hanukaev, Harley Eades
Type systems which account for resource sensitive computations can generally be split into two styles: First, substructural logics such as Linear Logic which seek to restrict weake…
A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
Victoria Vollmer, Danielle Marshall, Harley Eades +1
Graded modal logics generalise standard modal logics via families of modalities indexed by an algebraic structure whose operations mediate between the different modalities. The gra…
Combining dependency, grades, and adjoint logic
Peter Hanukaev, Harley Eades
We propose two new dependent type systems. The first, is a dependent graded/linear type system where a graded dependent type system is connected via modal operators to a linear typ…
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…
An Intuitionistic Linear Logical Semantics of SAND Attack Trees
Harley Eades
In this paper we introduce a new logical foundation of SAND attack trees in intuitionistic linear logic. This new foundation is based on a new logic called the Attack Tree Linear L…
Dialectica Categories for the Lambek Calculus
Valeria de Paiva, Harley Eades
We revisit the old work of de Paiva on the models of the Lambek Calculus in dialectica models making sure that the syntactic details that were sketchy on the first version got comp…
A Cointuitionistic Adjoint Logic
Harley Eades, Gianluigi Bellin
One leading question with respect to Bi-intuitionistic logic (BINT) is, what does BINT look like across the three arcs -- logic, typed -calculi, and category theory -- of the Cu…
Dualized Simple Type Theory
Harley Eades, Aaron Stump, Ryan McCleeary
We propose a new bi-intuitionistic type theory called Dualized Type Theory (DTT). It is a simple type theory with perfect intuitionistic duality, and corresponds to a single-sided…
Hereditary Substitution for the λΔ-Calculus
Harley Eades, Aaron Stump
Hereditary substitution is a form of type-bounded iterated substitution, first made explicit by Watkins et al. and Adams in order to show normalization of proof terms for various c…
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn +7
We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studi…