Coeffects Bibliography

Inspired by the collaborative effects bibliography, this is a collection of research papers and other resources related to coeffect tracking in programming languages theory and implementation. (This list intentionally excludes work on linear and other substructural logics, whose corpus is too vast to collect here.)

Contributing guidelines

• If you don't have push access, you can create a pull request.
• For publications, add an entry to this file and the coeffects.bib file, both sorted by date in newest → oldest order, then for ambiguous dates by article-insensitive alphabetical order (e.g. A Core Quantitative... comes after Bounded Linear...).
• Use formatting consistent with the existing files.

Software Projects

• Granule: A statically-typed linear functional language with graded modal types for fine-grained program reasoning.
  [website] [GitHub]

Papers and Preprints

2026

• Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types (ICFP 2026)
  Vilem-Benjamin Liepelt, Danielle Marshall, and Dominic Orchard
  [DOI] [arXiv (extended version)]

• Dependent Coeffects for Local Sensitivity Analysis (POPL 2026)
  Victor Sannier and Patrick Baillot
  [DOI] [HAL] [slides]

• Typing Strictness (POPL 2026)
  Daniel Sainati, Joseph W. Cutler, Benjamin C. Pierce, and Stephanie Weirich
  [DOI] [arXiv (extended version)]

• On Graded Coeffect Types for Information-Flow Control
  Vilem-Benjamin Liepelt, Danielle Marshall, Dominic Orchard, Vineet Rajani, and Michael Vollmer
  [DOI]

2025

• A Mixed Linear and Graded Logic: Proofs, Terms, and Models (CSL 2025)
  Victoria Vollmer, Danielle Marshall, Harley Eades III, and Dominic Orchard
  [DOI] [arXiv (extended version)]

2024

• Non-linear communication via graded modal session types
  Danielle Marshall and Dominic Orchard
  [DOI]

• Effects and Coeffects in Call-by-Push-Value (OOPSLA 2024)
  Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, and Stephanie Weirich
  [DOI] [arXiv (extended version)]

• Functional Ownership through Fractional Uniqueness (OOPSLA 2024)
  Danielle Marshall and Dominic Orchard
  [DOI] [appendices] [artefact]

• Program Synthesis from Graded Types (ESOP 2024)
  Jack Hughes and Dominic Orchard
  [DOI] [appendices]

2023

• Resource-Aware Soundness for Big-Step Semantics (OOPSLA 2023)
  Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca
  [DOI] [arXiv (extended version)]

• A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized (ICFP 2023)
  Andreas Abel, Nils Anders Danielsson, and Oskar Eriksson
  [DOI] [artefact] [GitHub]

• Combining Dependency, Grades, and Adjoint Logic (TyDe 2023)
  Peter Hanukaev and Harley Eades III
  [DOI] [arXiv]

• Multi-Graded Featherweight Java (ECOOP 2023)
  Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca
  [DOI] [arXiv (extended version)]

2022

• Graded Modal Types for Integrity and Confidentiality (PLAS 2022)
  Danielle Marshall and Dominic Orchard
  [DOI]

• Coeffects for Sharing and Mutation (OOPSLA 2022)
  Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca, and Marco Servetto
  [DOI] [arXiv (extended version)]

• Linearity and Uniqueness: An Entente Cordiale (ESOP 2022)
  Danielle Marshall, Michael Vollmer, and Dominic Orchard
  [DOI] [appendices]

• A Relational Theory of Effects and Coeffects (POPL 2022)
  Ugo Dal Lago and Francesco Gavazzo
  [DOI] [HAL]

2021

• Linear Exponentials as Graded Modal Types (TLLA 2021)
  Jack Hughes, Danielle Marshall, James Wood, and Dominic Orchard
  [HAL]

• Graded Modal Dependent Type Theory (ESOP 2021)
  Benjamin Moon, Harley Eades III, and Dominic Orchard
  [DOI] [arXiv (extended version)]

• A Graded Dependent Type System with a Usage-Aware Semantics (POPL 2021)
  Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich
  [DOI] [arXiv (extended version)]

2020

• Resourceful Program Synthesis from Graded Linear Types (LOPSTR 2020)
  Jack Hughes and Dominic Orchard
  [DOI]

• Deriving Distributive Laws for Graded Linear Types (TLLA 2020)
  Jack Hughes, Michael Vollmer, and Dominic Orchard
  [arXiv] [extended abstract]

• A Unified View of Modalities in Type Systems (ICFP 2020)
  Andreas Abel and Jean-Philippe Bernardy
  [DOI] [PDF (extended version)]

2019

• Quantitative Program Reasoning with Graded Modal Types (ICFP 2019)
  Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III
  [DOI] [PDF (extended version)]

2018

• Syntax and Semantics of Quantitative Type Theory (LICS 2018)
  Robert Atkey [DOI] [PDF]

• Call-by-need effects via coeffects
  Dylan McDermott and Alan Mycroft
  [DOI] [PDF]

• Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language (POPL 2019)
  Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack
  [DOI] [PDF (extended version)] [GHC wiki]

2016

• Combining Effects and Coeffects via Grading (ICFP 2016)
  Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu
  [DOI] [PDF]

• I Got Plenty o' Nuttin'
  Conor McBride
  [DOI] [PDF]

2014

• Bounded Linear Types in a Resource Semiring (ESOP 2014)
  Dan R. Ghica and Alex I. Smith
  [DOI] [PDF]

• A Core Quantitative Coeffect Calculus (ESOP 2014)
  Aloïs Brunel, Marco Gaboardi, Damiano Mazza & Steve Zdancewic
  [DOI] [PDF]

• Coeffects: a calculus of context-dependent computation (ICFP 2014)
  Tomáš Petříček, Dominic Orchard, and Alan Mycroft
  [DOI]

2013

• Coeffects: Unified Static Analysis of Context-Dependence (ICALP 2013)
  Tomáš Petříček, Dominic Orchard, and Alan Mycroft
  [DOI]

Theses and Dissertations

2026

• Graded Modal Types for Memory and Communication Safety (PhD thesis)
  Danielle Marshall
  [PDF]

2025

• Graded Modal Type Theory, Formalized (licentiate thesis)
  Oskar Eriksson
  [HDL] [PDF] [artefact]

2014

• Programming contextual computations (PhD thesis)
  Dominic Orchard
  [PDF]