pith. sign in

arxiv: 2606.28042 · v1 · pith:KIJALHQ4new · submitted 2026-06-26 · 💻 cs.PL

Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types

Vilem Liepelt , Danielle Marshall , Dominic Orchard This is my paper

Pith reviewed 2026-06-29 01:57 UTC · model grok-4.3

classification 💻 cs.PL
keywords graded typescoeffectslinear typesgraded modalitiestype translationscontext dependenceresource trackingtype systems
0
0 comments X

The pith

Translations show graded coeffect systems with pervasive annotations and those using modal operators on linear types express the same context dependencies.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper demonstrates that two separate styles of graded coeffect type systems can model identical forms of context dependence. One style places coeffect annotations directly on function types throughout a calculus. The other adds a graded modal operator to an underlying linear type system. By constructing translations between representative calculi in each style and proving they preserve typing, grading, and reduction steps, the work establishes that neither style is more or less expressive for tracking resources and effects.

Core claim

We answer this question by giving translations between pairs of calculi of both lineages that we prove type-, grade- and operational-semantics preserving. We show that the same notions of context dependence can be expressed in either style, building a bridge between the two lineages that enables transfer of results and ideas, while helping language designers to make better informed choices.

What carries the argument

The mutual translations between graded-base calculi (coeffect annotations on function types) and linear-base calculi (graded modal operator over linear types) that preserve typing judgments, grade annotations, and operational semantics.

If this is right

  • Proofs and results established in one lineage apply directly to the other via the translations.
  • Language designers can select either base structure without losing the ability to model particular context dependencies.
  • Operational behavior and resource accounting remain consistent when moving programs between the two styles.
  • Existing implementations in languages using one style can draw on techniques developed in the other.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The equivalence may allow hybrid systems that combine features from both bases without duplication of effort.
  • Future work on extending graded coeffects to new domains can target whichever base is mechanically simpler for the extension.
  • Tooling for type inference or program transformation could be shared across languages that adopt either style.

Load-bearing premise

The specific pairs of calculi chosen stand in for the full range of graded-base and linear-base systems that have appeared in the literature.

What would settle it

A concrete context-dependence property that can be typed and reduced in one style but has no corresponding typing or reduction sequence under the translation to the other style.

Figures

Figures reproduced from arXiv: 2606.28042 by Danielle Marshall, Dominic Orchard, Vilem Liepelt.

Figure 1
Figure 1. Figure 1: Relationship between graded calculi studied in this paper. For each calculus, a selection of representative [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Linear Base typing. et al. [2014]. The opposite polarity is also used in the literature, for example by Brunel et al. [2014], without any semantic difference. Example 2.4. The natural numbers semiring (N, ∗, 1, +, 0, ≡) whose ordering is equality (i.e., a discrete ordering) captures a notion of exact usage. For example, the following captures the typing of a linear function 𝑓 that takes two inputs of type … view at source ↗
Figure 3
Figure 3. Figure 3: Linear Base - Operational semantics and equations [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Graded Base system Definition 2.10 (Freshness). We make use of freshness here and throughout. It is defined as follows: 𝑥1, . . . , 𝑥𝑛#𝑡 ≜ {𝑥1, . . . , 𝑥𝑛} ∩ fv(𝑡) = ∅ 2.2 Graded Base The next calculus, Graded Base, is representative of the coeffect systems of Petricek et al. [2014, 2013], the generalised bounded linear type system of Ghica and Smith [2014], and the OO-based approach of Bianchini et al. [2… view at source ↗
Figure 5
Figure 5. Figure 5: Linear Core semantics and typing Syntax. We extend Linear Base and Graded Modal Base (which already share the same syntax) with the same extended syntax: t ::= ... | ⟨t1, t2⟩ | let ⟨x, y⟩ = t1 in t2 | ⟨⟩ | let ⟨⟩ = t1 in t2 | inj1 t | inj2 t | case t of {inj1 x → t1; inj2 y → t2} (terms) These additional term formers provide product introduction and elimination, unit introduction and elimination, and sum (… view at source ↗
Figure 6
Figure 6. Figure 6: Graded Modal Core additional typing rules. [PITH_FULL_IMAGE:figures/full_fig_p019_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Linear Push Core 5.6 Translation from Graded Modal Core to Linear Push Core We define the translation from Graded Modal Core into Linear Push Core as follows (fixing the unsound translation to Linear Core from Section 5.4 in the product and sum elimination): J ⟨t1, t2⟩ K ≜ ⟨Jt1K, Jt2K⟩ Jlet ⟨x, y⟩ = t1 in t2K ≜ let ⟨x ′ , y ′ ⟩ = push⊗ [Jt1K] in let [x] = x ′ in let [y] = y ′ in Jt2K Jinj1 t K ≜ inj1 JtK J… view at source ↗
read the original abstract

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 types for coeffects have found their way into languages such as Haskell, Idris, and Granule, enabling resourceful reasoning via coeffect analysis with varying levels of generality. Two separate lineages of graded coeffect system have emerged in the last decade: those in which coeffect annotations are pervasive, requiring annotations on function types (which we call graded-base) and those in which coeffects are added by way of a graded modal type operator atop linear types (which we call linear-base). The latter has its origins in Girard's Linear Logic which has been a rich humus for programming language research focused on resources, whereas the graded-base approach emerged in the mid-2010s, seeing rapid adoption in programming language theory and practice, e.g. in QTT and Linear Haskell. The relationship between these two styles has however remained an open question. We answer this question by giving translations between pairs of calculi of both lineages that we prove type-, grade- and operational-semantics preserving. We show that the same notions of context dependence can be expressed in either style, building a bridge between the two lineages that enables transfer of results and ideas, while helping language designers to make better informed choices.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The paper claims that the same notions of context dependence (coeffects) can be expressed in either the graded-base or linear-base style of graded type systems. It establishes this by defining type-, grade-, and operational-semantics-preserving translations between specific pairs of calculi drawn from each lineage.

Significance. If the translations are sound and the chosen calculi capture the essential structure of each lineage, the work provides a concrete bridge between two previously separate approaches to graded coeffects. This would enable transfer of results across lineages and give language designers clearer criteria for choosing between pervasive grade annotations and graded modal operators atop linear types.

major comments (2)
  1. [Abstract] Abstract: the claim that the translations show the same notions of context dependence are expressible in either style is load-bearing on the selected pairs being representative of the graded-base and linear-base lineages. The manuscript must explicitly state the features of the chosen calculi (arbitrary semirings, support for non-idempotent grades, multiple modalities, contraction rules, etc.) and argue why preservation results extend beyond the concrete instances.
  2. [Abstract] The abstract states that type-, grade-, and operational-semantics preservation have been proved, yet the full derivations, lemmas, and edge-case handling are not visible. Without these, it is impossible to verify that the translations are faithful for the full range of grades and reductions present in the source calculi.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and constructive feedback. We address the two major comments point by point below, indicating the revisions we will make to strengthen the manuscript.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim that the translations show the same notions of context dependence are expressible in either style is load-bearing on the selected pairs being representative of the graded-base and linear-base lineages. The manuscript must explicitly state the features of the chosen calculi (arbitrary semirings, support for non-idempotent grades, multiple modalities, contraction rules, etc.) and argue why preservation results extend beyond the concrete instances.

    Authors: We agree that the strength of the central claim depends on the representativeness of the chosen calculi. In the revised manuscript we will add an explicit subsection (likely in the introduction or a new 'Design Choices' section) that enumerates the supported features of both the graded-base and linear-base calculi, including arbitrary semirings, non-idempotent grades, multiple modalities, and contraction/weakening rules. We will also include a short argument explaining why the core structures captured by these calculi are representative of each lineage and why the preservation results are expected to extend to other systems sharing those structures. revision: yes

  2. Referee: [Abstract] The abstract states that type-, grade-, and operational-semantics preservation have been proved, yet the full derivations, lemmas, and edge-case handling are not visible. Without these, it is impossible to verify that the translations are faithful for the full range of grades and reductions present in the source calculi.

    Authors: The complete proofs, including all lemmas, derivations, and edge-case handling for the full range of grades and reductions, appear in the appendix of the current manuscript. To improve visibility we will add explicit forward references from the main text (in Sections 4 and 5) to the relevant appendix subsections and insert a concise high-level overview of the proof strategy for type, grade, and operational-semantics preservation in the body of the paper. revision: yes

Circularity Check

0 steps flagged

No circularity; translations and preservation proofs are original contributions between independent calculi

full rationale

The paper's central result consists of newly constructed type-, grade-, and operational-semantics-preserving translations between specific pairs of calculi drawn from the graded-base and linear-base lineages. These translations are presented and proved directly in the work rather than derived from or reduced to any prior equations, fitted parameters, or self-citations by the authors. The abstract and description indicate that the calculi are selected from existing independent literature, and the bridge is established by explicit mappings whose correctness is shown rather than assumed by definition or external self-referential uniqueness theorems. No step matches the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on standard background results from type theory and operational semantics for lambda calculi; no new free parameters, ad-hoc axioms, or invented entities are introduced.

axioms (1)
  • standard math Standard properties of type systems and operational semantics in lambda calculi
    The preservation proofs rely on these background results from prior type theory.

pith-pipeline@v0.9.1-grok · 5777 in / 1159 out tokens · 24463 ms · 2026-06-29T01:57:53.862795+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

39 extracted references · 24 canonical work pages · 1 internal anchor

  1. [1]

    ACM Program

    A unified view of modalities in type systems.Proc. ACM Program. Lang.4, ICFP (2020), 90:1–90:28. doi:10.1145/3408972 Andreas Abel, Nils Anders Danielsson, and Oskar Eriksson

    work page doi:10.1145/3408972 2020

  2. [2]

    ACM Program

    A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized.Proc. ACM Program. Lang.7, ICFP (2023), 920–954. doi:10.1145/3607862 Robert Atkey

    work page doi:10.1145/3607862 2023

  3. [3]

    InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12,

    Syntax and Semantics of Quantitative Type Theory. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12,

    2018

  4. [4]

    doi:10.1145/3209108.3209189 P

    56–65. doi:10.1145/3209108.3209189 P. N. Benton

    work page doi:10.1145/3209108.3209189

  5. [5]

    InComputer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers (Lecture Notes in Computer Science, Vol

    A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). InComputer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers (Lecture Notes in Computer Science, Vol. 933), Leszek Pacholski and Jerzy Tiuryn (Eds.). Springer, 121–135. doi:10.1007/BFB0022251 Jean-Philippe Bernardy...

    work page doi:10.1007/bfb0022251 1994

  6. [6]

    ACM Program

    Linear Haskell: practical linearity in a higher-order polymorphic language.Proc. ACM Program. Lang.2, POPL (2018), 5:1–5:29. doi:10.1145/3158093 Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. 2023a. Multi-Graded Featherweight Java. In37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Wa...

    work page doi:10.1145/3158093 2018

  7. [7]

    arXiv:2507.13792 doi:10.48550/ARXIV.2507.13792 Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca, and Marco Servetto

    Don’t exhaust, don’t waste.CoRR abs/2507.13792 (2025). arXiv:2507.13792 doi:10.48550/ARXIV.2507.13792 Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca, and Marco Servetto

    work page doi:10.48550/arxiv.2507.13792 2025

  8. [8]

    ACM Program

    Coeffects for sharing and mutation.Proc. ACM Program. Lang.6, OOPSLA2 (2022), 870–898. doi:10.1145/3563319 Edwin C. Brady. 2021a. Idris 2: Quantitative Type Theory in Practice. In35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference) (LIPIcs, Vol. 194), Anders Møller and Manu Sridharan (...

    work page doi:10.1145/3563319 2022

  9. [9]

    ACM Program

    A graded dependent type system with a usage-aware semantics.Proc. ACM Program. Lang.5, POPL (2021), 1–32. doi:10.1145/3434331 Soichiro Fujii, Shin-ya Katsumata, and Paul-André Melliès

    work page doi:10.1145/3434331 2021

  10. [10]

    Towards a Formal Theory of Graded Monads. InFoundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (Lecture Notes in Computer Science, Vol. 9634), Bart Ja...

    work page doi:10.1007/978-3-662-49630-5_30 2016

  11. [11]

    Combining effects and coeffects via grading. InProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 476–489. doi:10.1145/2951913.2951939 Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen D...

    work page doi:10.1145/2951913.2951939 2016

  12. [12]

    ACM Program

    Data Race Freedom à la Mode.Proc. ACM Program. Lang.9, POPL (2025), 656–686. doi:10.1145/3704859 Dan R. Ghica and Alex I. Smith

    work page doi:10.1145/3704859 2025

  13. [13]

    InProceedings of the 1986 ACM Conference on LISP and Functional Programming

    Integrating functional and imperative programming. InProceedings of the 1986 ACM Conference on LISP and Functional Programming. 28–38. Jean-Yves Girard

    1986

  14. [14]

    Jean-Yves Girard, Andre Scedrov, and Philip J Scott

    Linear logic.Theoretical computer science50, 1 (1987), 1–101. Jean-Yves Girard, Andre Scedrov, and Philip J Scott

    1987

  15. [15]

    Jack Hughes, Danielle Marshall, James Wood, and Dominic Orchard

    Bounded linear logic: a modular approach to polynomial-time computability.Theoretical computer science97, 1 (1992), 1–66. Jack Hughes, Danielle Marshall, James Wood, and Dominic Orchard

    1992

  16. [16]

    In5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021)

    Linear Exponentials as Graded Modal Types. In5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021). Rome (virtual), Italy (Jun 2021), https://hal-lirmm. ccsd. cnrs. fr/lirmm-03271465. 28 Jack Hughes and Dominic Orchard

    2021

  17. [17]

    Resourceful Program Synthesis from Graded Linear Types. InLogic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7-9, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12561), Maribel Fernández (Ed.). Springer, 151–170. doi:10.1007/978-3-030-68446- 4_8 Jack Hughes and Dominic Orchard

    work page doi:10.1007/978-3-030-68446- 2020

  18. [18]

    Program Synthesis from Graded Types. InProgramming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 14576), Stephanie Weirich (E...

    work page doi:10.1007/978-3-031-57262-3_4 2024

  19. [19]

    InProceed- ings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity&TLLA@IJCAR- FSCD 2020, Online, 29-30 June 2020 (EPTCS, Vol

    Deriving Distributive Laws for Graded Linear Types. InProceed- ings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity&TLLA@IJCAR- FSCD 2020, Online, 29-30 June 2020 (EPTCS, Vol. 353), Ugo Dal Lago and Valeria de Paiva (Eds.). 109–131. doi:10.4204/ EPTCS.353.6 Shin-ya Katsumata

    2020

  20. [20]

    Parametric effect monads and semantics of effect systems. InThe 41st Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 633–646. doi:10.1145/2535838.2535846 Vilem Liepelt, Danielle Marshall, Dominic Orchard, Michael Vollmer, and Vi...

    work page doi:10.1145/2535838.2535846 2014

  21. [21]

    Sam Lindley

    On Graded Coeffect Types for Information-Flow Control.Lecture Notes in Computer ScienceTo Appear (2024). Sam Lindley

    2024

  22. [22]

    ACM Program

    Oxidizing OCaml with Modal Memory Management.Proc. ACM Program. Lang.8, ICFP (2024), 485–514. doi:10.1145/3674642 John M Lucassen and David K Gifford

    work page doi:10.1145/3674642 2024

  23. [23]

    InProceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

    Polymorphic effect systems. InProceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 47–57. Conor McBride. 2016.I Got Plenty o’ Nuttin’. Springer International Publishing, Cham, 207–233. doi:10.1007/978-3-319- 30936-1_12 Eugenio Moggi

    work page doi:10.1007/978-3-319- 2016

  24. [24]

    doi:10.1109/LICS.1989.39155 Eugenio Moggi

    IEEE Computer Society, 14–23. doi:10.1109/LICS.1989.39155 Eugenio Moggi

    work page doi:10.1109/lics.1989.39155 1989

  25. [25]

    Comput.93, 1 (1991), 55–92

    Notions of Computation and Monads.Inf. Comput.93, 1 (1991), 55–92. doi:10.1016/0890-5401(91)90052- 4 B Moon, H Eades III, and D Orchard

    work page doi:10.1016/0890-5401(91)90052- 1991

  26. [26]

    Graded Modal Dependent Type Theory. InProgramming Languages and Systems30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27–April 1, 2021, Proceedings, Vol. 12648. 462–490. Alan Mycroft, Dominic A. Orchard, and Tomas Petricek

    2021

  27. [27]

    InSemantics, Logics, and Calculi - Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays (Lecture Notes in Computer Science, Vol

    Effect Systems Revisited - Control-Flow Algebra and Semantics. InSemantics, Logics, and Calculi - Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays (Lecture Notes in Computer Science, Vol. 9560), Christian W. Probst, Chris Hankin, and René Rydhof Hansen (Eds.). Springer, 1–32. doi:10.1007/978-3-319-27810-0...

    work page doi:10.1007/978-3-319-27810-0_1

  28. [28]

    Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III

    Type and effect systems.Principles of Program Analysis(1999), 283–363. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III

    1999

  29. [29]

    doi:10.1145/3341714 Dominic A

    Quantitative program reasoning with graded modal types.PACMPL3, ICFP (2019), 110:1–110:30. doi:10.1145/3341714 Dominic A. Orchard, Tomas Petricek, and Alan Mycroft

    work page doi:10.1145/3341714 2019

  30. [30]

    arXiv:1401.5391 http://arxiv.org/abs/1401.5391 Tomas Petricek, Dominic Orchard, and Alan Mycroft

    The semantic marriage of monads and effects.CoRR abs/1401.5391 (2014). arXiv:1401.5391 http://arxiv.org/abs/1401.5391 Tomas Petricek, Dominic Orchard, and Alan Mycroft

    Pith/arXiv arXiv 2014

  31. [31]

    InAutomata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II (Lecture Notes in Computer Science, Vol

    Coeffects: Unified Static Analysis of Context-Dependence. InAutomata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 7966), Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg (Eds.). Springer, 385–397. doi:10.1007/978-...

    work page doi:10.1007/978-3-642-39212-2_35 2013

  32. [32]

    The GHC Developers

    Call-by-name, call-by-value and the 𝜆-calculus.Theoretical computer science1, 2 (1975), 125–159. The GHC Developers. 2020.GHC User’s Guide: Linear Types. https://web.archive.org/web/20241206233933/https://downloads. haskell.org/ghc/9.0.1/docs/html/users_guide/exts/linear_types.html Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio...

    arXiv 1975

  33. [33]

    Schumacher, H

    Effects and Coeffects in Call-By-Push-Value (Extended Version).CoRRabs/2311.11795 (2023). arXiv:2311.11795 doi:10.48550/ARXIV. 2311.11795 29 Niki Vazou, Eric Seidel, Richard Eisenberg, Simon Peyton Jones, and Dimitrios Vytiniotis

    work page internal anchor Pith review doi:10.48550/arxiv 2023

  34. [34]

    https://icfp20.sigplan.org/details/hiw-2020- papers/1/Liquid-Haskell-as-a-GHC-Plugin Victoria Vollmer, Danielle Marshall, Harley Eades III, and Dominic Orchard

    2020

  35. [35]

    326 (2025), 32:1–32:21

    A Mixed Linear and Graded Logic: Proofs, Terms, and Models. 326 (2025), 32:1–32:21. doi:10.4230/LIPICS.CSL.2025.32 Philip Wadler and Peter Thiemann

    work page doi:10.4230/lipics.csl.2025.32 2025

  36. [36]

    David Walker

    The marriage of effects and monads.ACM Transactions on Computational Logic (TOCL)4, 1 (2003), 1–32. David Walker

    2003

  37. [37]

    James Wood and Robert Atkey

    Substructural type systems.Advanced topics in types and programming languages(2005), 3–44. James Wood and Robert Atkey

    2005

  38. [38]

    James Wood and Robert Atkey

    A linear algebra approach to linear metatheory.arXiv preprint arXiv:2005.02247(2020). James Wood and Robert Atkey

    arXiv 2005

  39. [39]

    A Framework for Substructural Type Systems. InProgramming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings (Lecture Notes in Computer Science, Vol. 13240), Ilya Sergey (Ed.). Springer, 376–4...

    work page doi:10.1007/978-3-030-99336-8_14 2022