Dependent types allow us to express precisely what a function is intended to do. Recent
work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also …

We present a graded modal type theory, a dependent type theory with grades that can be
used to enforce various properties of the code. The theory has Π-types, weak and strong Σ …

Graded modal types systems and coeffects are becoming a standard formalism to deal with
context-dependent, usage-sensitive computations, especially when combined with …

We introduce a general theory of quantitative and metric rewriting systems, namely systems
with a rewriting relation enriched over quantales modelling abstract quantities. We develop …

Substructural type systems are growing in popularity because they allow for a resourceful
interpretation of data which can be used to rule out various software bugs. Indeed …

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 …

We combine dependent types with linear type systems that soundly and completely capture
polynomial time computation. We explore two systems for capturing polynomial time: one …

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 …

Programmers can often improve the performance of their programs by reducing heap
allocations: either by allocating on the stack or reusing existing memory in-place. However …

We extend the semantics and type system of a lambda calculus equipped with common
constructs to be resource-aware. That is, reduction is instrumented to keep track of the …