Pith. sign in

REVIEW 4 major objections 4 minor 36 references

Typestate via Revocable Capabilities

T0 review · 4 major / 4 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Flow-sensitive typestate tracking rides on revocable capabilities, letting a Scala 3 extension reject stale state uses at compile time.

desk verdict A genuinely ergonomic typestate design with nice case studies, whose headline safety claim currently rests on an unpublished same-group formalization and an unproved Sigma/ANF bridge. read the letter →

arxiv 2510.08889 v2 pith:5RF64A4X submitted 2025-10-10 cs.PL

Songlin Jia , Craig Liu , Siyuan He , Haotian Deng , Yuyan Bao , Tiark Rompf This is my paper
classification cs.PL
keywords typestaterevocablecapabilitiesdestructiveeffectsreachabilitytypespath-dependentimplicitresolutionANFtransformationsession
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Flow-sensitive typestate tracking can be built on top of flow-insensitive capability mechanisms, rather than requiring a bespoke typestate analysis. The central trick is to decouple capability lifetimes from lexical scopes, so functions can receive, revoke, and return capabilities in a flow-sensitive way; a destructive effect system kills stale capabilities and any reachable aliases, path-dependent types tie each capability to a specific object's identity, and a type-directed ANF transformation returns fresh capabilities into implicit scope. The paper implements this as a Scala 3 compiler prototype and demonstrates it on file operations, hand-over-hand locking, DOM construction with context-free bracket states, and binary session types. If the claim holds, ordinary imperative code gets compile-time rejection of write-after-close and similar illegal state uses without explicit state annotations.

What carries the argument

The central mechanism is the revocable capability: a token whose type is path-dependent on a specific resource (e.g., f.IsOpen) and whose lifetime is governed by a destructive effect system. The arrows ?=> (capability received implicitly), =!> (capability revoked/killed), and ?<= (capability returned implicitly) are combined as ?=!>? to express a complete typestate transition in a function type. A transient Σ-pair bundles a resource with a fresh capability for return, and a type-directed ANF transformation immediately unpacks it, placing the capability into implicit scope with highest precedence so that implicit resolution automatically finds the current state and not a stale one. This machi

What would settle it

Compile a program that stores an open-file capability in a mutable variable, closes the file through the original variable, then reads through the stored capability. The paper's Section 5 openly omits destructive effects on mutable variables and object fields, so if this program type-checks and throws a file error at runtime, the claimed static safety does not extend to ordinary imperative code; similarly, any accepted program that performs a write-after-close via an alias or escape would falsify the central claim.

Watch

Extended reading notes

Core claim

The paper shows that stateful resource safety can be enforced by turning capabilities into first-class, revocable witnesses of an object's current state. Each resource (file, lock, DOM node, channel) carries abstract type members for its states, and a capability is a path-dependent value of one of those state types. Operations consume and reissue capabilities: an open-file capability is killed by close, and a fresh closed-file capability is returned; because the new capability is numerically tied to the same object via its path prefix, capabilities for different objects can never be confused. The system's three arrows — implicit receive (?=>), destructive revoke (=!>), and implicit return (?

Load-bearing premise

Safety rests on the assumption that the prototype's adaptations to the formally proved effect system — omitting the separate tracking of use versus mention, adding the FUN self-reference marker, and translating Sigma-pairs in continuation-passing style — preserve that system's soundness; the paper states but does not prove this.

Editorial extensions

If this is right

  • Programs that use a resource after a state transition — writing to a closed file, unlocking a lock that was never acquired, closing a DOM element twice — fail to type-check.
  • Capabilities can be released out of LIFO order, so patterns like hand-over-hand locking compile and are statically verified.
  • The same framework covers finite-state resources and context-free typestate such as balanced DOM bracket stacks, by parameterizing a type member over a compile-time list.
  • Binary session types become typestate capabilities: protocol violations on channel endpoints, including sending after the channel is closed or selecting an unavailable branch, are caught statically.
  • Because capabilities are resolved implicitly, user code stays concise and aliasing is handled by qualifier/disjointness checks rather than explicit permission annotations.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the omitted destructive effects on mutable variables and object fields are added, the same mechanism could plausibly subsume ownership and borrow checking for a broader class of imperative Scala code, not just resource protocols.
  • The transient Σ-pair plus ANF unpacking is a reusable pattern: any capability-based language with path-dependent types and implicit resolution could adopt flow-sensitive typestate without a bespoke whole-program analysis.
  • A natural stress test would apply the prototype to existing Scala code that uses synchronized and resource-handling libraries, measuring how many idioms require new annotations and how often the checker's conservative qualifier tests reject safe code.
  • A mechanized proof of soundness for the prototype's actual core subset — including the FUN self-reference and CPS-transformed Sigma — would convert the imported guarantee from an assumption into a theorem; until then the safety result is contingent.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper proposes a design for flow-sensitive typestate tracking in Scala 3 by extending flow-insensitive capability mechanisms. The central mechanism is a destructive effect arrow (=!>), an implicit-return arrow (?<=) implemented via a type-directed ANF transformation over transient Sigma pairs, and path-dependent capabilities to preserve resource identity. The paper claims that these minimal extensions make imperative typestate programming statically safe and ergonomic, and it supports this with several case studies: file operations, hand-over-hand locking, DOM construction, and binary session types. A prototype compiler extension and a brief informal account of the underlying formal model are presented, with the soundness argument delegated to the same-group formalization of Deng et al. [2025].

Significance. If the claims were fully established, the paper would make a useful practical contribution: it would show that a small, mostly library-level extension to an existing mainstream language can express a wide range of typestate patterns without the explicit annotations of earlier typestate systems. The breadth of the case studies (locks, DOM, sessions) and the fact that the prototype is evaluated against the Scala capture-checker test suite (Section 5) are genuine strengths. However, the paper's central safety guarantee is not proved or even precisely stated for the actual implementation. The formal model of Deng et al. [2025] is imported, while the paper's own novel device—Sigma-guided implicit return via ANF—is explicitly admitted to fall outside that formalism. The implementation also restricts itself to a core subset of Scala and uses unchecked `asInstanceOf` casts. As it stands, the paper does not deliver a self-contained, verifiable argument that the prototype is statically safe, and the printed case-study code is not independently reproducible. The contribution is promising, but the validation is incomplete.

major comments (4)
  1. [Section 4, "Sigma" paragraph] The paper states that "Sigma is not directly expressible using reachability types" and that "functions returning Sigma should be transformed in continuation-passing style," yet the actual implementation uses a type-directed ANF transform. No theorem, lemma, or even precise statement connects the implemented transform to the CPS translation, and no argument shows that the transient-wrapper discipline prevents the original Sigma pair or its fields from being used after an extracted capability is killed. Since the implicit-return arrow ?<= is implemented through this transform, the central claim of statically safe returning of capabilities is unsupported. A formal statement of the CPS translation and its relationship to the ANF transform, together with a proof or at least a precise soundness conjecture with a testable invariant, is needed.
  2. [Section 5, "Destructive Effect Checker"] The checker "supports a core subset of Scala 3" and "the most relevant omissions are destructive effects on mutable variables and object fields." This is a load-bearing limitation, not a footnote: the case studies in Section 3 are imperative and rely on mutable state—for instance, the Table and Row classes in Figure 2 have mutable lock fields, and the DOM example has internal state implied by "more fields" in Figure 4. The paper's abstract and introduction claim "static safety reasoning for expressive imperative code," but the implementation cannot track destructive effects on exactly the mutable fields that these examples use. The limitations need to be stated in the abstract/introduction and their impact on the case-study claims must be analyzed.
  3. [Section 3 vs. §2.5 footnote 1] Section 3 states: "All code in this section can be compiled by our prototype." But §2.5 footnote 1 says that, due to a Scala limitation, "the implicit parameter c must be explicitly bound and passed" and that "for clarity, we omit them in subsequent examples." Therefore the printed code is not complete as shown and the claim is not independently checkable from the paper. Please provide a complete artifact, or show all code snippets in compilable form (even if verbose), and mark which portions are elided.
  4. [Section 4, "One-Shot Functions"] The paper introduces a static marker FUN to denote "the self-reference at the innermost (most recent) level," deviating from Deng et al. [2025], who use explicit naming for multiple levels of self-reference. This extension is used in Section 3.3.1 for `cFuture`, where a callback must be allowed to kill free variables. No soundness argument shows that the innermost-level self-reference is equivalent to the original multi-level mechanism, or that the interaction of FUN with the destructive effect checker preserves the imported soundness result. This is another adaptation that needs either a formal account or an explicit reduction to the existing formalism.
minor comments (4)
  1. [Throughout] There are several typos: "posesses" (§3.3), "chanenl" (§3.3.1), "protcool" (§3.3), and inconsistent use of "Section 3.2" where a figure reference is intended for `open`/`close` (§3.2). A pass for terminology consistency would help.
  2. [Section 2.4] The presentation of path-dependent capabilities would benefit from an explicit comparison of the `^` tracking notation with the `q` freshness marker used in the formal model; the two notations are mixed in Section 2.1.2 and later, which can mislead readers about which formal system is being followed.
  3. [Section 3.3, Figure 8] The definition of `Dual` via match types is only sketched (`typeDual[P <: Session] <: Session = Pmatch`). Since the session-type case study relies on duality being type-level and sound, please clarify the omitted match cases and any bounds needed for `Var[N <: Int]`.
  4. [Section 5] The paper says the prototype can also be implemented as a compiler plugin, but no artifact or repository is provided. For a paper whose main evidence is a working prototype, making the code available would substantially strengthen the evaluation and reproducibility.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the core safety anchor is prior formal work (Deng et al. 2025), and the Sigma/ANF extension is asserted rather than proved, but nothing in the derivation is equivalent to its own inputs by construction.

full rationale

Walking the derivation chain, I find no step in which a prediction or first-principles result is equivalent to its inputs by construction. The formal safety anchor is Deng et al. [2025], a prior formalization of reachability types with destructive effects; although the author list overlaps with the present paper, it is a separate formal system with stated assumptions (System F<: plus higher-order references), not a restatement of the present paper's target claim, so it counts as independent support rather than a circular input. The genuinely new mechanisms—path-dependent capabilities, Sigma-based returning, and the type-directed ANF transform—are presented as design extensions, not derived from the target safety claim. Section 4 explicitly limits the formal link: 'Sigma is not directly expressible using reachability types' and says functions returning Sigma 'should be transformed in continuation-passing style,' while Section 5 describes a type-directed ANF transform without proving equivalence to that CPS translation. This is an unproven soundness gap and a correctness risk, especially for uses after Sigma unpacking, but it is not circular: no equation or fitted quantity is re-labelled as a prediction. Similarly, Section 5's caveat that the checker supports only a core subset omitting destructive effects on mutable variables and object fields narrows the scope of the claim, and footnote 1 of Section 2.5 means the printed examples are not fully self-contained; these affect reproducibility and completeness, not circularity. The conservative omission of the 'use' effect in Section 4 is explicitly an over-approximation, so it cannot smuggle in the safety conclusion by construction. The case studies are empirically checkable against the prototype, which is external evidence rather than a circular step. Overall, the appropriate finding is no significant circularity.

Assumptions & free parameters 0 free parameters · 5 assumptions · 4 invented entities

No numerical free parameters appear; this is a type-system/compiler design rather than an empirical fit. The ledger records the unproved or borrowed assumptions: the central safety guarantee depends on (a) Deng et al.'s destructive effect system, (b) conservative use approximation, (c) Sigma/ANF semantics, (d) hidden casts hidden by opaque type members, and (e) FUN self-reference.

assumptions (5)
  • domain assumption Deng et al. 2025 destructive effect system for reachability types is sound and applies to the core used here.
    Section 4 builds on this formalization; it is cited, not proved in this paper, and its authors overlap with this paper's authors.
  • domain assumption Conservative approximation of use effects by reachability qualifiers is sound.
    Section 4: "we simplify this aspect by omitting the explicit use effect component, instead conservatively approximating usage through the mentioning information encoded in reachability qualifiers." No proof is supplied in this paper.
  • ad hoc to paper Sigma can be treated as a transient wrapper with immediate unpacking; CPS/ANF transformation preserves typing and semantics.
    Section 4: Sigma is not expressible in reachability types; functions returning Sigma "should be transformed in continuation-passing style." No formal soundness theorem is given.
  • ad hoc to paper The singleton-type ascription and Unit instantiation of abstract type members are safe despite hidden asInstanceOf casts.
    Figures 3 and 5 use "safe type cast" to Unit-instantiated capabilities; safety relies on opacity of the type members and is not formally verified.
  • ad hoc to paper FUN self-reference for one-shot function kills is sound at the innermost (most recent) level.
    Section 4: "we employ a static notation, FUN..." This deviates from Deng et al.'s explicit naming, and no proof is provided.
invented entities (4)
  • @kill(...) effect annotation / destructive arrow =!>
    purpose: Flow-sensitive revocation of capabilities, invalidating stale handles after state transitions.
    Introduced to invalidate stale capabilities; no external falsifiable handle beyond the paper's own compiler examples.
  • Sigma transient dependent pair
    purpose: Bundle a resource and its path-dependent capability while preserving type-level dependency.
    Explicitly marked transient and requiring immediate unpacking; no runtime representation and no formal semantics in this paper.
  • implicit result arrow ?<= and composite arrow ?=!>?
    purpose: Return capabilities for implicit resolution at the call site after a state transition.
    New notation backed by the Sigma-guided ANF transform; formal semantics are not fully specified.
  • FUN self-reference marker
    purpose: Allow one-shot functions to express the killing of captured free variables.
    Static shorthand for self-referential qualifiers; soundness is asserted, not proven.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Typestate via Revocable Capabilities." pith.science (2026). https://pith.science/paper/5RF64A4X

@misc{pith2026251008889,
  author       = {Pith},
  title        = {Pith review of: Typestate via Revocable Capabilities},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5RF64A4X}},
  note         = {Machine review of arXiv:2510.08889}
}
read the original abstract

Managing stateful resources safely and expressively is a longstanding challenge in programming languages, especially in the presence of aliasing. For example, scope-based constructs like Java's synchronized blocks offer ease of reasoning, but they restrict expressiveness and parallelism. Conversely, imperative, flow-sensitive approaches enable fine-grained control, but they require sophisticated typestate analyses and often burden programmers with explicit state tracking. In this work, we present a novel approach that unifies the ease of scoped reasoning with the expressiveness of imperative typestate management. Our design extends traditional flow-insensitive capability mechanisms to a flow-sensitive setting. In particular, we decouple capability lifetimes from lexical scopes, allowing functions to receive, revoke, or return capabilities in a flow-sensitive manner, building on existing mechanisms for the safety and ergonomics of scoped capability programming. We implement our approach as an extension to the Scala 3 compiler, leveraging path-dependent types and implicit resolution to enable concise, statically safe, and expressive typestate programming. Our prototype generically supports a wide range of patterns, including file operations, advanced locking protocols, DOM construction, and session types, showing that expressive and safe typestate management can be achieved with minimal extensions to an existing language with capability support.

Figures

Figures reproduced from arXiv: 2510.08889 by the authors.

Figure 1
Figure 1. A database transaction expressed in two different styles, where we first [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Table Locking Definitions 11 object Table: 12 def apply(n: Int): Sigma { type A = Table; type B = a.IsReleased^ } = // factory method 13 val table = new Table(n) { type IsReleased = Unit; type IsHeld = Unit } 14 new Sigma { 15 type A = Table; type B = a.IsReleased^ 16 val a: table.type = table 17 val b: a.IsReleased^ = () // Opaque outside of apply 18 } 19 20 extension (table: Table) 21 def lock(): table.IsReleased … view at source ↗
Figure 3
Figure 3. Table Locking API Line 20 defines a collective extension for a table: Table parameter, indicting that the methods lock, unlock, locateRow, and lockRow can all be used in the style of table.lock(). Methods that perform typestate transitions use ?=!>?. For example, method lock on line 21 changes the state of the Table by acquiring the lock. The implementation of all state-transitioning methods will return a Sigma with… view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: depicts the definitions for tracking open brackets. Tracking a list of open brackets necessitates defining list of DOM elements. First, a sum type Elem (line 1) is defined with a variant per element node. Then a list TList (line 6) can be defined to Elem. Note that TLi…
Figure 5
Figure 5. Figure 5: DOM Tree API 1 makeDOM { tree => ts => 2 tree.open(DIV())(using ts) 3 tree.close(DIV()) 4 tree.close(DIV()) // Error 5 } (a) Error on line 3, due to use of killed variable with type tree.Elems[DIV :: TNil] 1 makeDOM { tree => ts => 2 tree.open(DIV())(using ts) 3 tree.c…
Figure 8
Figure 8. Figure 8: Session Type Definitions Representing Session Types. The core session type definitions ( [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]
Figure 9
Figure 9. Figure 9: Channel API The methods recPush (line 50), recTop (line 51), and recPop (line 52) carry out protocol recursion as described in Section 3.3. When the protocol is Rec[P], recPush can be used to push P onto the channel environment E. If the protocol is Var-typed, it is ei…
Figure 10
Figure 10. Figure 10: Echo program implementation. The method return types are omitted. [PITH_FULL_IMAGE:figures/full_fig_p016_10.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

36 extracted references · 2 linked inside Pith

  1. [2025]

    ACM Program

    Modeling Reachability Types with Logical Relations – Semantic Type Soundness, Termination, Effect Safety, and Equational Theory.Proc. ACM Program. Lang.OOPSLA2 (2025). Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, and Tiark Rompf

    2025

  2. [5]

    ACM Program

    Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back.Proc. ACM Program. Lang.6, OOPSLA (2022), 1–30. Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann

    2022

  3. [8]

    Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies. Proc. ACM Program. Lang.7, OOPSLA2, Article 236 (oct 2023), 31 pages. Olivier Danvy and Andrzej Filinski

    2023

  4. [11]

    Surv.54, 5 (2022), 98:1–98:38

    Bidirectional Typing.ACM Comput. Surv.54, 5 (2022), 98:1–98:38. Andrzej Filinski

    2022

  5. [16]

    Polymorphic Iterable Sequential Effect Systems.ACM Trans. Program. Lang. Syst.43, 1 (2021), 4:1–4:79. Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf

    2021

  6. [17]

    arXiv:2509.04253 [cs] Fritz Henglein, Henning Makholm, and Henning Niss

    When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking. arXiv:2509.04253 [cs] Fritz Henglein, Henning Makholm, and Henning Niss

    arXiv

  7. [20]

    arXiv:2404.08217 [cs] Oleg Kiselyov and Hiromi Ishii

    Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types. arXiv:2404.08217 [cs] Oleg Kiselyov and Hiromi Ishii

    arXiv

  8. [22]

    InOOPSLA

    Typestate-like analysis of multiple interacting objects. InOOPSLA. ACM, 347–366. Martin Odersky et al. 2023.Scala 3 Reference - Capture Checking. https://docs.scala-lang.org/scala3/reference/experimental/ cc.html Martin Odersky et al . 2025.Separation Checking. https://nightly.scala-lang.org/docs/reference/experimental/capture- checking/separation-checkin...

    2023

Show all 36 references
  1. [25]

    ACM Program

    Borrowing From Session Types.Proc. ACM Program. Lang.OOPSLA2 (2025). Hannes Saffrich and Peter Thiemann

    2025

  2. [26]

    Methods Comput

    Relating Functional and Imperative Session Types.Log. Methods Comput. Sci.18, 3 (2022). Hannes Saffrich and Peter Thiemann

    2022

  3. [27]

    ACM Program

    Linearly qualified types: generic inference for capabilities and uniqueness.Proc. ACM Program. Lang.6, ICFP (2022), 137–164. Robert E. Strom and Shaula Yemini

    2022

  4. [29]

    Data types à la carte.J. Funct. Program.18, 4 (2008), 423–436. Kaku Takeuchi, Kohei Honda, and Makoto Kubo

    2008

  5. [30]

    Modal Effect Types. Proc. ACM Program. Lang.9, OOPSLA1 (2025), 1130–1157. Matías Toro and Éric Tanter

    2025

  6. [33]

    ACM Program

    Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs.Proc. ACM Program. Lang.8, POPL (2024), 393–424. Anxhelo Xhebraj, Oliver Bračevac, Guannan Wei, and Tiark Rompf

    2024

  7. [34]

    ACM Program

    Degrees of Separation: A Flexible Type System for Safe Concurrency.Proc. ACM Program. Lang.8, OOPSLA1 (2024), 1181–1207. Yichen Xu, Oliver Bračevac, Nguyen Pham, and Martin Odersky

    2024

  8. [35]

    ACM Program

    What’s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures.Proc. ACM Program. Lang.OOPSLA2 (2025). Yichen Xu and Martin Odersky

    2025

  9. [36]

    arXiv:2306.06496 [cs]

    Formalizing Box Inference for Capture Calculus. arXiv:2306.06496 [cs]

    arXiv

  10. [1966]

    ACM9, 3 (1966), 143–155

    Programming semantics for multiprogrammed computations.Commun. ACM9, 3 (1966), 143–155. Jana Dunfield and Neel Krishnaswami

    1966

  11. [1986]

    IEEE Trans

    Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Trans. Software Eng.12, 1 (1986), 157–171. Wouter Swierstra

    1986

  12. [1987]

    Linear Logic.Theor. Comput. Sci.50 (1987), 1–102. Colin S. Gordon

    1987

  13. [1992]

    Representing Control: A Study of the CPS Transformation.Math. Struct. Comput. Sci.2, 4 (1992), 361–391. Robert DeLine and Manuel Fähndrich

    1992

  14. [1993]

    In Proceedings of the ACM SIGPLAN’93 Conference on Programming Language Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June 23-25, 1993, Robert Cartwright (Ed.)

    The Essence of Compiling with Continuations. In Proceedings of the ACM SIGPLAN’93 Conference on Programming Language Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June 23-25, 1993, Robert Cartwright (Ed.). ACM, 237–247. Ronald Garcia, Éric Tanter, Roger Wolff...

    1993

  15. [2003]

    The marriage of effects and monads.ACM Trans. Comput. Log.4, 1 (2003), 1–32. Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, and Tiark Rompf

    2003

  16. [2006]

    Type checking a multithreaded functional language with session types.Theor. Comput. Sci.368, 1-2 (2006), 64–87. Philip Wadler

    2006

  17. [2008]

    Effective typestate verification in the presence of aliasing.ACM Trans. Softw. Eng. Methodol.17, 2 (2008), 9:1–9:34. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen

    2008

  18. [2014]

    ACM Trans

    Foundations of Typestate-Oriented Programming. ACM Trans. Program. Lang. Syst.36, 4 (2014), 12:1–12:44. Simon J. Gay, Vasco Thudichum Vasconcelos, António Ravara, Nils Gesbert, and Alexandre Z. Caldeira

    2014

  19. [2015]

    InProceedings of the 11th ACM SIGPLAN Workshop on Generic Programming(Vancouver, BC, Canada)(WGP 2015)

    Session types for Rust. InProceedings of the 11th ACM SIGPLAN Workshop on Generic Programming(Vancouver, BC, Canada)(WGP 2015). Association for Computing Machinery, New York, NY, USA, 13–22. Typestate via Revocable Capabilities 23 Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao...

    2015

  20. [2016]

    Surv.49, 1 (2016), 3:1–3:36

    Foundations of Session Types and Behavioural Contracts.ACM Comput. Surv.49, 1 (2016), 3:1–3:36. Mathias Jakobsen, Alice Ravier, and Ornela Dardha

    2016

  21. [2017]

    ACM Program

    Simplicitly: Foundations and Applications of Implicit Function Types.Proc. ACM Program. Lang.2, POPL (Dec. 2017), 42:1–42:29. Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondrej Lhoták

    2017

  22. [2018]

    ACM Program

    Effect handlers for the masses.Proc. ACM Program. Lang.2, OOPSLA (2018), 111:1–111:27. Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann

    2018

  23. [2019]

    InProceedings 12th Interaction and Concurrency Experience, ICE 2019, Copenhagen, Denmark, 20-21 June 2019 (EPTCS, Vol

    Rusty Variation: Deadlock-free Sessions with Failure in Rust. InProceedings 12th Interaction and Concurrency Experience, ICE 2019, Copenhagen, Denmark, 20-21 June 2019 (EPTCS, Vol. 304), Massimo Bartoletti, Ludovic Henrio, Anastasia Mavridou, and Alceste Scalas (Eds.). 48–60. ...

    2019

  24. [2020]

    Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala.J. Funct. Program.30 (2020), e8. Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf

    2020

  25. [2021]

    ACM Program

    Reachability types: tracking aliasing and separation in higher-order functional programs.Proc. ACM Program. Lang.5, OOPSLA (2021), 1–32. Kevin Bierhoff and Jonathan Aldrich

    2021

  26. [2022]

    ACM Program

    Type-level programming with match types.Proc. ACM Program. Lang.6, POPL, Article 37 (Jan. 2022), 24 pages. Aleksander Boruch-Gruszecki, Martin Odersky, Edward Lee, Ondrej Lhoták, and Jonathan Immanuel Brachthäuser

    2022

  27. [2023]

    Capturing Types.ACM Trans. Program. Lang. Syst.45, 4 (2023), 21:1–21:52. John Boyland

    2023

  28. [2024]

    ACM Program

    Law and Order for Typestate with Borrowing.Proc. ACM Program. Lang.8, OOPSLA2 (2024), 1475–1503. Hannes Saffrich, Janek Spaderna, Peter Thiemann, and Vasco T. Vasconcelos

    2024

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.