5 papers
Categorical Models of Amortized Cost: An Adjoint Relationship between Cost and Potential
David Binder, David Corfield, Dominic Orchard +1
Various type systems have been developed to track the cost of a computation using a cost-tracking monad . On its own, this only tracks the worst-case cost of a computati…
Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types
Vilem Liepelt, Danielle Marshall, Dominic Orchard
Graded types provide a way to augment a type system with fine-grained information, e.g., to track side effects or context dependence and resource use (called coeffects). Graded typ…
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…
Functional Ownership through Fractional Uniqueness
Danielle Marshall, Dominic Orchard
Ownership and borrowing systems, designed to enforce safe memory management without the need for garbage collection, have been brought to the fore by the Rust programming language.…
Graded Modal Types for Integrity and Confidentiality
Danielle Marshall, Dominic Orchard
Graded type systems, such as the one underlying the Granule programming language, allow various different properties of a program's behaviour to be tracked via annotating types wit…