Pith. sign in

REVIEW 3 major objections 4 minor 51 references

Kindly Bent to Free Us

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

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

Pith's one-line read A single ML-like language now combines Rust-style borrowing, linearity, and principal type inference.

desk verdict A credible combination of Rust-style borrows and linear/affine kinds with principal inference, held back by two openly flagged but unproved elaboration steps; worth serious refereeing, not rejection. read the letter →

arxiv 1908.09681 v4 pith:VAG3XZNA submitted 2019-08-26 cs.PL

Gabriel Radanne , Hannes Saffrich , Peter Thiemann This is my paper · ORCID
classification cs.PL
keywords lineartypesaffineborrowingregioninferenceconstrainedprincipaltypesubstructuralML
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

Affe is an extension of ML that aims to make resource management statically safe without changing how programs are written. The paper's central claim is that linearity and affinity can be encoded as kinds attached to ordinary types, and that Rust-style borrowing—exclusive borrows for mutation, shared borrows for read access—can be confined to lexical regions while retaining the ML property of complete principal type inference. If the claim is right, a systems programmer can mix functional and imperative code over resources like file handles, arrays, and connection pools, and the type checker will reject duplication, leaks, use-after-free, and mutation through shared views. The paper backs the claim with a formal type system over a kind lattice, a type-soundness theorem against a big-step semantics that counts uses and tracks permissions, and an inference algorithm proven to compute principal types. No linearity annotations are needed in expressions; region annotations are inserted automatically.

What carries the argument

The load-bearing device is the indexed kind lattice $Q_n$ for $Q\in\{U,A,L\}$—unrestricted, affine, linear—ordered $U\le A\le L$, with the index $n$ recording the lexical nesting level of a region. Kinds annotate function arrows and borrowed types, so multiplicity is a property of types and of closures, not of the expression syntax. A region expression $\{|e|\}^n_{x\mapsto b}$ transforms a suspended binding for $x$ into a borrow binding for the body, and the splitting rules for environments decide which bindings can be duplicated, discarded, or only used as borrows. On top of this, the HM(X) framework—a Hindley-Milner inference scheme for constrained types—supplies the normalization, unification, and simplification machinery that yields principal types; the automatic region pass inserts the explicit regions before typing.

What would settle it

Take a surface program that uses two conflicting borrows of the same variable in a branch, e.g., an exclusive borrow in each arm of a conditional, with no explicit regions, and feed it to the automatic annotation pass from the prototype; if the pass diverges, emits overlapping regions, or rejects code whose hand-annotated equivalent is accepted by the internal type system, then the automatic-borrowing claim is refuted.

Watch

Extended reading notes

Core claim

On its own terms, the paper establishes that a strict, impure ML-like language can carry linearity, affinity, and borrowing in its types rather than in the program text. A declared type like `File.t : lin` makes every handle linear, so omitting `close` is a type error; writing to the handle takes an exclusive borrow $\&!h$, whose type is affine, so a closure capturing it can be called at most once, while shared borrows $\&a$ are unrestricted inside their region and can be duplicated. Regions are lexical, and the kind index $n$ is the nesting depth: the constraint $(\tau \le L_{n-1})$ on a region body ensures that nothing typed deep inside the region can escape to an enclosing level. The type system is a conservative extension of the HM(X) constrained-type framework, the inference algorithm instantiates HM(X) and returns principal types with constraint simplification, and soundness is stated with respect to a big-step semantics whose permissions track exactly which uses remain available.

Load-bearing premise

The automatic pass that inserts explicit region annotations must always succeed and must never change which programs typecheck, but the paper only sketches an informal growth heuristic and a rewriting relation without proving termination, confluence, or preservation of typability.

Editorial extensions

If this is right

  • APIs can be written in direct resource-passing-free style: `fopen` returns a linear handle, `close` consumes it, and omitting the close is a static error rather than a runtime discipline.
  • Borrows are contained: an exclusive borrow cannot be duplicated and a shared borrow cannot mutate, so a region body cannot leak a borrowed value outward; a linear resource can be freed only after all regions using it have ended.
  • Inference stays readable: the inferred type of application is $(\alpha^\kappa\to\beta)\to(\alpha^\kappa\to\beta)$, and composition prints as $(\kappa\le\kappa_1)\Rightarrow(\beta^\kappa\to\gamma)\to(\alpha^{\kappa_1}\to\beta)^\kappa\to(\alpha^{\kappa_1}\to\gamma)$, with subsumption absorbing the expected join constraint.
  • The linearity-aware big-step semantics gives strong invariants: linear resources are freed exactly once, permissions are withdrawn when a closure or resource is consumed, and locations outside the reachable environment are unchanged by the frame condition.
  • The prototype covers algebraic datatypes, pattern matching, and conditionals, so the formal core extends beyond the minimal internal language.

Reading between the lines

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

  • The unproved automatic region-annotation pass is the boundary between the surface language and the typed core; proving termination, confluence, and typability preservation, or folding region placement into constraint solving, would make the automatic-borrowing claim airtight.
  • Affe's examples of arrays and pools suggest a reusable pattern for persistent data structures with transient mutation: the type system certifies in-place update on an exclusive borrow and copy-on-write on a shared borrow, a contract that could be packaged as a library API for garbage-collected languages.
  • The paper's discussion of non-lexical lifetimes hints that replacing lexical regions with per-expression live-borrow annotations would move the system closer to Rust's behavior; testing that variant against the existing examples would show whether inference survives the change.
  • A safe exclusive element-borrow primitive like `get_eb` appears to require existential region identities; implementing it would put a concrete price on Affe's decision to keep principal inference.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

Summary. The paper presents Affe, an ML-like language whose type system manages linearity and affinity through a kind lattice, constrained kinds, and lexical regions, with exclusive and shared borrowing inspired by Rust. The core of the paper is a formal internal language with explicit regions, a syntax-directed type system, a big-step operational semantics with permissions and explicit resource bookkeeping, and a type inference algorithm built on the HM(X) framework. The authors claim complete principal type inference without user-provided linearity annotations, automatic region inference for borrows, and an expressive type soundness theorem. The paper also includes a prototype implementation and several substantial examples including file handles, mutable arrays, a Sudoku solver, session types, and a pool of resources.

Significance. If the technical claims are fully established, this is a significant contribution to substructural type systems: it demonstrates a design point that combines affine and linear types, shared and exclusive borrows, lexical regions, and principal type inference in an ML-like language, which none of the closely related systems (Linear Haskell, Quill, Alms, Mezzo, Rust) achieves on all axes. The formal development is unusually thorough for a systems-oriented PL paper: the internal type system and inference rules are given in detail, the constraint solver is defined with proofs of principal normal forms and regularity, and the semantics is designed so that the soundness theorem can state resource-specific invariants such as no-thin-air permissions and the frame condition. The prototype and playground are concrete reproducibility assets. The main weaknesses are two load-bearing proof gaps, discussed below: the automatic region annotation pass is not proved to preserve typability, and the type soundness proof is restricted to A-normal forms without a proved ANF elaboration.

major comments (3)
  1. [§3.2 and Appendix B (Fig. 17)] The automatic region annotation pass e↝e′ is the bridge between the surface language and the typed internal language, but the paper does not prove termination, confluence, or preservation/reflection of typability for this rewriting relation. The rules in Fig. 17 are given without a decreasing measure or a normal-form argument, and the structural properties asserted at the end of §3.2 (well-nested annotations, at most one region per borrow, exactly one region per exclusive borrow) are stated but not derived from the rules. Since the pass runs before typing, a surface program's typeability and its inferred principal type depend on this transformation. If two reduction orders yield different annotations with different typability, the surface claim of automatic region inference is not even well-defined. A preservation theorem of the form 'if p↝p′ and p′ is typeable in the internal language, then p is typeable in the surface language', together with a determinacy or confluence result, is needed to support the contributions 'automatic inference of regions' and 'does not require any linearity annotations in expressions'.
  2. [§5.1 and Appendix G] Theorem 5.1 is stated for the general internal language and for the eval relation of Section 3.4, but the first paragraph of Appendix G restricts the proof to terms in A-normal forms following the grammar e ::= . . . | (x x′) | (x,x′)k | matchϕ x,x′ = z in e. No translation from general terms to ANF is defined, and no lemma is proved that such a translation preserves typing and semantics. Consequently the type soundness theorem as stated is not proved for general applications, general pairs, or general match expressions. The statement of Theorem 5.1 must be restricted to ANF, or an ANF elaboration with typing- and semantics-preservation proofs must be supplied, before the soundness claim covers the language actually defined in Section 3.
  3. [§4.4 and Appendix E] The principal-inference completeness proof is presented as an adaptation of Sulzmann's HM(X) completeness proof, with several cases summarized as 'the rest of the proof follows HM(X)'. The authors do provide the key statements and some case analyses, so this is not an omission of the same severity as the two gaps above. However, because the extension includes kind inference, usage environments, environment splitting, and borrowing rules, a reader cannot fully verify from the appendix that the HM(X) machinery transfers unchanged. I would ask the authors to make the dependence on the cited proof explicit and to state which of the HM(X) lemmas are reused verbatim and which are genuinely new, so that the completeness claim can be checked without reconstructing the full argument from the citation.
minor comments (4)
  1. [§1.2] The contribution bullet claims that the type system is 'a conservative extension of systems for existing ML-like languages', but no base system or embedding theorem is defined anywhere in the paper. Please either formalize this claim or qualify it to avoid a mathematically imprecise statement.
  2. [§2.3] The primitive get_eb is marked '(* Unsafe! *)' in the text and then presented alongside the safe primitives. Since the formal type system of Section 3 does not include array primitives at all, clarify whether get_eb is an unsafe library primitive, a proposed extension, or merely an illustrative type that the safe system would reject.
  3. [Fig. 14] In the comparison matrix, the 'Escape hatch' column for Affe is marked with partial support (~) and the caption says this feature is available but not formalized, yet no escape hatch is described in the body of the paper. Either add a brief discussion or change the table entry to avoid overclaiming.
  4. [§1] The text contains the typo 'seemlessly' in the first paragraph; it should read 'seamlessly'.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the formal type system, inference algorithm, and soundness proof are self-contained; the main gaps are omitted proofs, not circular reductions.

full rationale

The paper's central claims are the design of Affe's kind-constrained type system, its HM(X)-based principal type inference, and an expressive type soundness theorem. None of these reduce to their own inputs by construction. The inference rules in Appendix E are proved sound and complete with respect to the syntax-directed type system (Theorems E.5 and E.11), with the proofs adapted from the external HM(X) literature rather than from the authors' own prior results. The constraint system CL is given an explicit normalization algorithm and a proof of principal normal forms in Appendix C, so inference does not presuppose the theorem it is meant to establish. The type soundness theorem (Theorem 5.1) is proved by induction on the big-step evaluation in Appendix G using independently stated store typing and permission invariants. The only noteworthy weaknesses are not circularity but omitted proofs. Section 3.2 says, 'We give an informal presentation of our code transformation and defer the complete definition to Appendix B,' and Appendix B defines the rewriting relation without proving termination, confluence, or preservation of typability. Similarly, Appendix G begins, 'For simplicity, we only consider terms in A-normal forms following the grammar,' while Theorem 5.1 is stated for general terms. These are load-bearing gaps for the automatic region insertion and full-language soundness claims, respectively, but they do not make any derived quantity equal to an input or rename a fitted parameter as a prediction. The paper also relies on external, non-self citations such as HM(X) [26] and Sulzmann [39], and the prototype is used as an implementation artifact rather than as circular evidence. No fitted parameters, no self-citation chains, and no equivalence-by-construction steps were found.

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

There are no fitted numerical parameters: Affe is a type system defined by rules, not by data fitting. The main load-bearing premises are the kind lattice, the HM(X) framework, the A-normal form restriction used in the soundness proof, and the well-formedness of borrow modifier stacks. The automatic region annotation pass is the least supported premise, since it is presented as an algorithm but lacks termination and typability-preservation theorems.

assumptions (4)
  • domain assumption The kind lattice U <= A <= L with region levels Qn and Qn <= Qn' for n <= n' correctly models resource multiplicity and nesting.
    This lattice, defined in Fig. 6, is the foundation of all typing rules: it fixes when values may be duplicated, dropped, or used exactly once, and how borrow regions are ordered. The paper does not derive it from more basic principles.
  • standard math HM(X) guarantees principal type inference when the constraint system is regular and normalization computes principal normal forms.
    The paper relies on Odersky et al. [26] for the HM(X) framework and adapts it to kind inference, affine types, and borrows in Section 4 and Appendix E. This is a prior theorem, not proved inside the paper.
  • domain assumption Every well-typed surface term can be put into A-normal form without changing typing or evaluation semantics.
    Appendix G states 'For simplicity, we only consider terms in A-normal forms' but does not prove that the full language is covered by this restriction. The type soundness theorem is therefore established only for that subset.
  • domain assumption Borrow modifier stacks are well-formed, with all unrestricted modifiers before all affine modifiers, and borrow compatibility matches the runtime checks.
    Appendix G uses this modeling choice to relate environment splitting, store typing, and permissions. It is a plausible semantic model, but it is assumed rather than derived.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Kindly Bent to Free Us." pith.science (2026). https://pith.science/paper/VAG3XZNA

@misc{pith2026190809681,
  author       = {Pith},
  title        = {Pith review of: Kindly Bent to Free Us},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VAG3XZNA}},
  note         = {Machine review of arXiv:1908.09681}
}
read the original abstract

Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities. While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper handling of resources. An important step towards handling resources is the adoption of linear and affine types that enforce single-threaded resource usage. However, the few languages supporting such types require heavy type annotations. We present Affe, an extension of ML that manages linearity and affinity properties using kinds and constrained types. In addition Affe supports the exclusive and shared borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: it is an impure, strict, functional expression language with complete principal type inference and type abstraction. Affe does not require any linearity annotations in expressions and supports common functional programming idioms.

Figures

Figures reproduced from arXiv: 1908.09681 by the authors.

Figure 1
Figure 1. Writing files (4) Neither LH nor Quill have borrowing whereas Affe supports two flavors: affine (exclusive, mutable) and unrestricted (shared, immutable) borrows. See Section 7 for further in-depth discussion of these and other related works. 1.1 First examples As a first, well-known example we consider a simplified API for writing files shown in Fig. 1a. It introduces a linear abstract type File.t. A call like File… view at source ↗
Figure 2
Figure 2. Linear arrays Affe relies on the notion of borrowing [8]. Our first example of linear arrays demonstrates simple borrowing and imperative programming; the second example demonstrates reborrowing and the interaction between closures and borrowing by implementing a Sudoko solver based on a hybrid copy-on-write data structure; the third example demonstrates advanced uses of regions with iter￾ators on linear values and … view at source ↗
Figure 3
Figure 3. Signature and Implementation of hybrid arrays [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (25 more)
Figure 4
Figure 4. Figure 4: Excerpt of the Sudoku solver structure. The module CowArray, also in [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: Syntax The rest of this section formalizes Affe: the syntax (Section 3.1), the statics in terms of a re￾gion annotation pass (Section 3.2) and syntax-directed typing (Section 3.3), and a dynamics that is linearity- and resource-aware (Section 3.4). 3.1 Syntax [PITH_FU…
Figure 6
Figure 6. Figure 6: La ice ordering – k ≤L k ′ Γ ::= · | Γ; B (Environments) B ::= ∅ (Empty) | (α : θ) (Types) | (x : σ) (Variables) | [x : σ] n b (Suspended) | (x ÷ σ) k b (Borrows) [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]
Figure 8
Figure 8. Figure 8: Spli ing rules for bindings – C ⊢e B = Bl ⋉ Br C | Γ ⊢s e : τ — Expression e has type τ in environment Γ under constraints C. C | Γ ⊢s τ : k — Type τ has kind k in environment Γ under constraints C. D ⊢e C — Constraint D entails constraint C. D =e C — Constraints C and…
Figure 9
Figure 9. Figure 9: Selected typing rules (C | Γ ⊢s e : τ ) and borrowing rules (C ⊢e Γ x n Γ ′ ) Rule Var looks up the type scheme of the variable x in the environment Γ and instantiates it with Inst(Γ, σ). Instantiation follows the HM(X) formulation and takes as input a scheme σ and an …
Figure 10
Figure 10. Figure 10: Syntax of internal language Let-polymorphism in the surface language gives rise to elaborated letfun expressions anno￾tated with a type scheme σ and a kind k indicating their usage restriction (linear, affine, etc) rela￾tive to the variables and constraints of σ. Thei…
Figure 11
Figure 11. Figure 11: Big-step interpretation operator acts as monadic bind for the sem monad. The operator let∗? : bool −→ ( unit −→ α sem ) −→ α sem converts a boolean argument into success or failure in the monad. 1 let (let*?) : bool −→ (unit −→ β sem) −→ β sem = 2 fun b f −→ if b then…
Figure 12
Figure 12. Figure 12: Selected inference rules – Σ |(C,ψ) | Γ ⊢w e : τ Environments and Bindings. In the syntax-directed system, the Var rule ensure that linear vari￾ables are not discarded at the leaves. In the inference algorithm, we operate in the opposite direc￾tion: we collect data fr…
Figure 13
Figure 13. Figure 13: Graph representing the example constraints [PITH_FULL_IMAGE:figures/full_fig_p019_13.png]
Figure 14
Figure 14. Figure 14: Comparison matrix That is, if a thread closes over a borrow, that thread should have terminated before the parent thread leaves the borrow’s region. Rust addresses this lifetime issue with the move qualification for a thread which transfers ownership of the free varia…
Figure 15
Figure 15. Figure 15: Corresponding session type programs in Affe [PITH_FULL_IMAGE:figures/full_fig_p031_15.png]
Figure 16
Figure 16. Figure 16: The Pool module {x 7→ b} ⊕ · = · , {x 7→ b} , · AnnotRegion-Left · ⊕ {x 7→ b} = · , {x 7→ b} , · AnnotRegion-Right {x 7→ U} ⊕ {x 7→ U} = · , {x 7→ U} , · AnnotRegion-Immut {x 7→ U} ⊕ {x 7→ A} = {x 7→ U} , {x 7→ A} , · AnnotRegion-MutLeft {x 7→ A} ⊕ {x 7→ b} = {x 7→ A}…
Figure 17
Figure 17. Figure 17: Automatic region annotation — e e ′ e can be rewritten as a fully annotated term e ′ . Through the rule Rewrite-Top, this is defined in term of an inductively defined relation e n e ′ , S where n is the current nesting and S is a set of variable that are not yet enclo…
Figure 18
Figure 18. Figure 18: The constraint language l ≤L l ′ ⊢e(l ≤ l ′ ) ∀i, C ⊢e(li ≤ k) C ⊢e(∧i li ≤ k) ∀i, C ⊢e(k ≤ li) C ⊢e(k ≤ ∨i li) C ⊢e(k ≤ k ′ ) ∧ (τ ≤ τ ′ ) C ⊢e(& b (k, τ ) ≤ & b (k ′ , τ ′ )) C ⊢e(τ ′ 1 ≤ τ1) C ⊢e(τ2 ≤ τ ′ 2 ) C ⊢e(k ≤ k ′ ) C ⊢e(τ1 k −→τ2 ≤ τ ′ 1 k’ −→τ ′ 2 ) ∀i, C…
Figure 19
Figure 19. Figure 19: Base entailment rules – C ⊢e D which collects each variable that has a corresponding borrow. At each step, it rewrites the inner subterms, consider which borrow must be enclosed by a region now, and return the others for later enclosing. Binders force immediate enclos…
Figure 20
Figure 20. Figure 20: Syntax-directed kinding rule – C | Γ ⊢s τ : k Let us consider C = (k, k ′ ) ∈ R′′ 1 . Since C ′′ 1 =e C ′′ 2 , we have C ′′ 2 ⊢e C. If 0e C, by P(C ′′ 2 ) we have that C ∈ R ′′ 2 . If ⊢eC, then C ∈ (≤) ⊂ R ′′ 2 . We conclude that R ′′ 1 ⊂ R ′′ 2 . By symmetry, R ′′ 1 …
Figure 21
Figure 21. Figure 21: Spli ing — environments C ⊢e Γ = Γl ⋉ Γr ; inference C ⇚ Γ = Γl ⋉ Γr ; binders C ⇚ b = br ⋉ bl EBorrow Cr ⇚ [x : τ ] n b x n b Cr ⇚ Γ; [x : τ ] n b x n Γ; b EBorrow-Check C ⊢e D D ⇚ Γ; [x : τ ] n b x n Γ; b C ⊢e Γ; [x : τ ] n b x n Γ; b EBorrow-Binder b ∈ {U,A} C = (b…
Figure 22
Figure 22. Figure 22: Borrowing — environments C ⊢e Γ x n Γ ′ ; inference C ⇚ Γ x n Γ ′ ; binders C ⇚ b x n b ′ D.2 Environments In Section 3.3, we only gave a partial description of the splitting and borrowing relations on en￾vironments, C ⊢e Γ = Γ ⋉ Γ and C ⊢e Γ x n Γ. The complete defin…
Figure 23
Figure 23. Figure 23: Rewriting constraints on environments — (Γ ≤ k) { C Instance σ = ∀κi∀(αj : kj). C ⇒τ ψ = [κi 7→ ki , αj 7→ τj] ψ(C),ψ(τ ) = Inst(Γ, σ) Var (x : σ) ∈ Γ Cx , τx = Inst(Γ, σ) C ⊢e Cx ∧ (Γ\{x} ≤ A∞) C | Γ ⊢s x : τx Pair C ⊢e Γ = Γ1 ⋉ Γ2 C | Γ1 ⊢s e1 : τ1 C | Γ2 ⊢s e2 : τ2…
Figure 24
Figure 24. Figure 24: Syntax-directed typing rules – C | Γ ⊢s e : τ , Vol. 1, No. 1, Article . Publication date: June 2020 [PITH_FULL_IMAGE:figures/full_fig_p039_24.png]
Figure 25
Figure 25. Figure 25: Syntax-directed typing rules for internal language [PITH_FULL_IMAGE:figures/full_fig_p040_25.png]
Figure 26
Figure 26. Figure 26: Kind inference rules – (C,ψ) | Γ ⊢w τ : k E TYPE INFERENCE In this appendix, we provide the complete type inference rules and show that our type inference algorithm is sound and complete. The constraints rules are already shown in Section 4. Kind in￾ference is present…
Figure 27
Figure 27. Figure 27: Type inference rules – Σ |(C,ψ) | Γ ⊢w e : τ of local variables inside the constraints. This allows us to encapsulate all the quantified variables in the global constraints. It also reflects the fact that there should exist at least one solution for C for the scheme t…
Figure 28
Figure 28. Figure 28: Big-step interpretation , Vol. 1, No. 1, Article . Publication date: June 2020 [PITH_FULL_IMAGE:figures/full_fig_p048_28.png]
Figure 29
Figure 29. Figure 29: Big-step interpretation (resources) – ∆(ℓ) = T τ. • It remains to characterize unrestricted resources. Define unr∆(ℓ) if neither aff∆(ℓ) nor lin∆(ℓ) holds. • Relating environments to contexts ∆ ⊢ γ L ,γ A,γ U,γ A # ,γ U # : Γ. Here we consider an environment γ = (γ L …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

51 extracted references · 39 canonical work pages

  1. [1]

    Plasmeijer

    Peter Achten and Marinus J. Plasmeijer. 1995. The Ins and Outs of Clean I/O. J. Funct. Program. 5, 1 (1995), 81–110. https://doi.org/10.1017/S0956796800001258

    work page doi:10.1017/s0956796800001258 1995

  2. [2]

    Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Spar ks. 2009. Typestate-oriented programming. In Companion to the 24th Annual ACM SIGPLAN Conference on Objec t-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009, October 25-29, 2009, Orlando, F lorida, USA, Shail Arora and Gary T. Leavens (Eds.). ACM, 1015–1022. https://d...

    work page arXiv 2009

  3. [3]

    Nada Amin and Tiark Rompf. 2017. Type Soundness Proofs With Definit ional Interpreters. In POPL. ACM, 666–679

    work page 2017

  4. [4]

    Phil Bagwell. 2001. Ideal Hash Trees

    work page 2001

  5. [5]

    Thibaut Balabonski, François Pottier, and Jonathan Protzenko. 20 16. The Design and Formalization of Mezzo, a Permission-Based Programming Language. ACM Trans. Program. Lang. Syst. 38, 4 (2016), 14:1–14:94. http://dl.acm.org/citation.cfm?id=2837022

    work page 2016

  6. [6]

    Erik Barendsen and Sjaak Smetsers. 1995. Uniqueness Type Infere nce. In Programming Languages: Implementations, Logics and Programs, 7th International Symposium, PLILP’9 5, Utrecht, The Netherlands, September 20-22, 1995, Procee d- ings (Lecture Notes in Computer Science) , Manuel V. Hermenegildo and S. Doaitse Swierstra (Eds.), Vol. 982. Springer, 189–20...

    work page doi:10.1007/bfb0026821 1995

  7. [7]

    Newton, Simo n Peyton Jones, and Arnaud Spiwack

    Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simo n Peyton Jones, and Arnaud Spiwack. 2018. Linear Haskell: Practical Linearity in a Higher-Order Polymorphic La nguage. PACMPL 2, POPL (2018), 5:1–5:29. https://doi.org/10.1145/3158093

    doi:10.1145/3158093 2018

  8. [8]

    John Tang Boyland and William Retert. 2005. Connecting Effects and Uniq ueness with Adoption. In Pro- ceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Princi ples of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005 , Jens Palsberg and Martín Abadi (Eds.). ACM, 283–295. https://doi.org/10.1145/1040305.1040329

    arXiv 2005

Show all 51 references
  1. [9]

    Sylvain Conchon and Jean-Christophe Filliâtre. 2007. A Persiste nt Union-Find Data Structure. In Proceedings of the ACM Workshop on ML, 2007, Freiburg, Germany, October 5, 2007 , Claudio V. Russo and Derek Dreyer (Eds.). ACM, 37–46. https://doi.org/10.1145/1292535.1292541

    2007

  2. [10]

    Robert DeLine and Manuel Fähndrich. 2001. Enforcing High-Level Pr otocols in Low-Level Software. In PLDI. ACM, 59–69

    2001

  3. [11]

    Stephen Dolan, Spiros Eliopoulos, Daniel Hillerström, Anil Mad havapeddy, K. C. Sivaramakrishnan, and Leo White

  4. [12]

    Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. 2014. Foundations of Typestate-Oriented Programming. ACM Trans. Program. Lang. Syst. 36, 4 (2014), 12:1–12:44. https://doi.org/10.1145/262960 9

    2014 doi

  5. [13]

    Gay and Vasco Thudichum Vasconcelos

    Simon J. Gay and Vasco Thudichum Vasconcelos. 2010. Linear typ e theory for asynchronous session types. J. Funct. Program. 20, 1 (2010), 19–50. https://doi.org/10.1017/S0956796809 990268

    2010 doi

  6. [14]

    Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci. 50 (1987), 1–102. https://doi.org/10.1016/0304-3975(87)90045-4

    1987 doi

  7. [15]

    Gregory Morrisett, Trevor Jim, Michael W

    Dan Grossman, J. Gregory Morrisett, Trevor Jim, Michael W. H icks, Yanling Wang, and James Cheney. 2002. Region- Based Memory Management in Cyclone. In Proceedings of the 2002 ACM SIGPLAN Conference on Programmi ng Lan- guage Design and Implementation (PLDI), Berlin, Germany, ...

    2002

  8. [16]

    Rich Hickey. 2017. clojure/PersistentHashMap.java. http s://github.com/richhickey/clojure/blob/master/src/jvm/clojure/lang/PersistentHashMap.java

    2017

  9. [17]

    Kohei Honda. 1993. Types for Dyadic Interaction. In Proceedings of 4th International Conference on Concurrency Theory (LNCS), Eike Best (Ed.). Springer Verlag, 509–523

    1993

  10. [18]

    Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Held as Part of the European Joint Co...

    1998

  11. [19]

    Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and De rek Dreyer. 2018. RustBelt: Securing the Foundations of the Rust Programming Language. Proc. ACM Program. Lang. 2, POPL (2018), 66:1–66:34. https://doi.org/10.1145/3158154

    2018 doi

  12. [20]

    Garrett Morris

    Sam Lindley and J. Garrett Morris. 2017. Lightweight Functional S ession Types. In Behavioral Types: From Theory to Tools, Simon Gay and António Ravara (Eds.). River Publishers

    2017

  13. [21]

    Matsakis and Felix S

    Nicholas D. Matsakis and Felix S. Klock II. 2014. The Rust Lang uage. In Proceedings of the 2014 ACM SIGAda an- nual conference on High integrity language technology, HIL T 2014, Portland, Oregon, USA, October 18-21, 2014 , Michael Feldman and S. Tucker Taft (Eds.). ACM, 103–1...

    2014

  14. [22]

    Kazutaka Matsuda. 2019. A Modular Inference of Linear Types for Multiplicity-Annotated Arrows. CoRR abs/1911.00268 (2019). arXiv:1911.00268 http://arxiv.org /abs/1911.00268

    2019 arXiv

  15. [23]

    Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. 2010. Light weight Linear Types in System F°. In Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Wo rkshop on Types in Languages Design and Implementation, Madrid, Spain, January 23, 2010 , Andrew Kennedy and Nick Bent...

    2010

  16. [24]

    Garrett Morris

    J. Garrett Morris. 2016. The Best of Both Worlds: Linear Func tional Programming Without Compromise. In Proceedings of the 21st ACM SIGPLAN International Conferen ce on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 , Jacques Garrigue, Gabriele Keller, a...

    2016

  17. [25]

    Guillaume Munch-Maccagnoni. 2018. Resource Polymorphism. CoRR abs/1803.02796 (2018). arXiv:1803.02796 http://arxiv.org/abs/1803.02796

    2018 arXiv

  18. [26]

    Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999. Type Inference with Constrained Types. TAPOS 5, 1 (1999), 35–55

    1999

  19. [27]

    Martin Odersky, Philip Wadler, and Martin Wehr. 1995. A Second Look at Overloading. In Proceedings of the seventh in- ternational conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995 , John Williams (E...

    1995

  20. [28]

    Myreen, Ramana Kumar, and Yong Kiam Tan

    Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. 20 16. Functional Big-Step Semantics. In ESOP (Lecture Notes in Computer Science) , Vol. 9632. Springer, 589–615

  21. [29]

    Luca Padovani. 2017. A Simple Library Implementation of Binary S essions. J. Funct. Program. 27 (2017), e4. https://doi.org/10.1017/S0956796816000289

    2017 doi

  22. [30]

    François Pottier and Vincent Simonet. 2002. Information Flow Infere nce for ML. In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Program ming Languages, Portland, OR, USA, January 16-18, 2002, John Launchbury and John C. Mitchell (Eds.). AC...

    2002

  23. [31]

    Jonathan Protzenko. 2014. Mezzo: a typed language for safe effectful concurrent programs. (Mezzo: un langage typé pour programmer de manière concurrent et sure en présence d’effet s). Ph.D. Dissertation. Paris Diderot University, France. https://tel.archives-ouvertes.fr/tel-01086106

    2014

  24. [32]

    Juan Pedro Bolívar Puente. 2017. Persistence for the Masses : RRB-Vectors in a Systems Language. PACMPL 1, ICFP (2017), 16:1–16:28. https://doi.org/10.1145/3110260

    2017 doi

  25. [33]

    Reynolds

    John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Cope nhagen, Denmark, Proceedings . IEEE Computer Society, 55–74. https://doi.org/10.1109/LICS.2002.1029817

    2002 arXiv

  26. [34]

    Jeremy Siek. 2013. Type Safety in Three Easy Lemmas. http://siek.blogspot.de/2013/05/type-safety-in-three-easy-l emmas.html

    2013

  27. [35]

    Vincent Simonet. 2003. An extension of HM(X) with bounded existentia l and universal data-types. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functio nal Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, Colin Runciman and Olin Shivers (Eds.)...

    2003

  28. [36]

    Vincent Simonet. 2003. Type Inference with Structural Subtyping: A Faithful Formalization of an Efficient Con- straint Solver. In Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, Novem- ber 27-29, 2003, Proceedings (Lecture Notes in Computer ...

    2003 doi

  29. [37]

    Vincent Simonet and François Pottier. 2007. A Constraint-Based Appr oach to Guarded Algebraic Data Types. ACM Trans. Program. Lang. Syst. 29, 1 (2007), 1. https://doi.org/10.1145/1180475.1180476

    2007

  30. [38]

    Christian Skalka and François Pottier. 2002. Syntactic Type Sou ndness for HM(X). Electr. Notes Theor. Comput. Sci. 75 (2002), 61–74. https://doi.org/10.1016/S1571-0661(04)8 0779-5

    2002 doi

  31. [39]

    Martin Sulzmann. 1997. Proofs of soundness and completeness of type inference for H M (X). Technical Report. Research Report YALEU/DCS/RR-1102, Yale University, Department of Computer Science

    1997

  32. [40]

    Tov and Riccardo Pucella

    Jesse A. Tov and Riccardo Pucella. 2011. Practical affine type s. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 201 1, Austin, TX, USA, January 26-28, 2011 , Thomas Ball , Vol. 1, No. 1, Article . Publication date: June 2020...

    2011

  33. [41]

    Valery Trifonov and Scott F. Smith. 1996. Subtyping Constrained T ypes. In Static Analysis, Third International Sympo- sium, SAS’96, Aachen, Germany, September 24-26, 1996, Proceedings (Lecture Notes in Computer Science) , Radhia Cousot and David A. Schmidt (Eds.), Vol. 1145. ...

    1996 doi

  34. [42]

    consumes

    Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal A hmed. 2019. Oxide: The Essence of Rust. CoRR abs/1903.00982 (2019). arXiv:1903.00982 http://arxiv.org /abs/1903.00982 , Vol. 1, No. 1, Article . Publication date: June 2020. Kindly Bent to Free Us 31 A FURTHER EXA...

    2019 arXiv

  35. [44]

    best-effort

    C⊢e(k≤k′) C⊢e(τ1 k − →τ2≤τ′ 1 k’ −→τ′ 2) ∀i, C⊢e(τi =τi) C⊢e(Tτi≤ Tτ′ i) ≤ transitive, reflexive Fig. 19. Base entailment rules – C⊢eD which collects each variable that has a corresponding borrow. At each step, it rewrites the inner subterms, consider which borrow must be enclo...

    2020

  36. [45]

    Indeed, since C′ 1 andC′ 2 are only composed of existential quantifications and kind inequalit ies, the only rules that applies are transitivity and lattice inequalities

    hold. Indeed, since C′ 1 andC′ 2 are only composed of existential quantifications and kind inequalit ies, the only rules that applies are transitivity and lattice inequalities. After step (2) and (5), the associated relations are fully saturated for these two rules, hence all i...

    2020

  37. [46]

    If⊢eC, thenC∈(≤)⊂ R′′ 2

    we have thatC∈ R′′ 2 . If⊢eC, thenC∈(≤)⊂ R′′ 2 . We conclude that R′′ 1 ⊂ R′′ 2 . By symmetry, R′′ 1 = R′′ 2 and C′′ 1 =C′′ 2 . This equality is preserved by step (7) and (8) since the transiti ve reduction of a directed acyclic graph is unique, which concludes. □ We can now p...

    2020

  38. [47]

    C| Γ2;(x :ϕ(τ1));(/y.alt:ϕ(τ′ 1))⊢ se2 :τ2 C| Γ⊢s matchϕ x,x′ =sp e1 ine2 :τ2 Fig. 25. Syntax-directed typing rules for internal language –C| Γ⊢se :τ , Vol. 1, No. 1, Article . Publication date: June 2020. Kindly Bent to Free Us 41 KA/r.sc/r.sc (True,∅)| Γ⊢wτ1 k − →τ2 :k KB/o....

    2020

  39. [48]

    We also have that Σx\{x}⊂ Γx

    σ = gen(C, Γx ;(x :α),τ1) LetCa =C∧( Σ≤ κ)∧ Weak(x :α)(Σx) and By definition, ψD\{α;κ}≤ ϕD fv(Γx) ψ which means we haveψD\{α;κ}≤ ϕ◦ϕD fv(Γx) ψ′. We also have that Σx\{x}⊂ Γx . Since C⊢e(Γ′ x ≤ k), we have C⊢eψ′(Σ ≤ κ). If x ∈ Σx , then Weak(x :α)(Σx) = True. Other- wise we can ...

  40. [49]

    σ1 = gen(C, Γ1,τ1) , Vol. 1, No. 1, Article . Publication date: June 2020. 46 Gabriel Radanne, Hannes Saffrich, and Peter Thiemann and Σ 2|(C2,ψ2)|⇓ Γ2⊢we :τ2 ψ2≤ϕ2 fv(Γ)ψ′ 2 C′⊢eϕC2 ⊢eϕ2σ2≼ σ′ 2 Σ 2⊂ Γ2 σ′ 2 = gen(C′, Γ′ 2,τ′

    2020

  41. [50]

    We know that⊢eψ′Γ≼ Γ′,⊢eψ′ i Γi≼ Γ′ i and Σi⊂ Γi

    σ2 = gen(C, Γ2,τ2) By Lemmas E.8 and E.10, we have Σ 1|(C1,ψ1)|⇓ Γ⊢we :τ1 Σ 2|(C2,ψ2)|⇓ Γ⊢we :τ2 LetCs⇚ Σ = Σ 1 ⋉ Σ 2. We know that⊢eψ′Γ≼ Γ′,⊢eψ′ i Γi≼ Γ′ i and Σi⊂ Γi . By Lemma E.9, we haveC⊢eψ′Cs . The rest of the proof follows HM(X). □ C/o.sc/r.sc/o.sc/l.sc/l.sc/a.sc/r.sc/...

    2020

  42. [51]

    Kindly Bent to Free Us

    and ∆′ = ∆ : (A1-1) C| Γ2(x :τ1)(x′ :τ′ 1)⊢ se2 :τ2 by inversion (A1-2) ∆⊢ γ2 : Γ2 by assumption; moreover, ∆⊢ r1 : τ1 and ∆⊢ r′ 1 : τ′ 1 by inversion of the store typing for ℓ. As ∆′ = ∆ , we have ∆′⊢γ′ 2 : Γ2(x :τ1)(x′ :τ′ 1). (A1-3)⊢δ′ : ∆′ : the only change from assumption...

    2020 arXiv

  43. [2017]

    Concurrent System Programming with Effect Handlers. In Trends in Functional Programming - 18th International Symposium, TFP 2017, Canterbury, UK, June 19-21, 2017, Revi sed Selected Papers (Lecture Notes in Computer Science) , Meng Wang and Scott Owens (Eds.), Vol. 10788. Sprin...

    2017 doi

Pith tools

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