Thread and Memory-Safe Programming with CLASS

TL;DR

This work addresses safe, deadlock-free, terminating concurrent programming by presenting CLASS, a proof-of-concept language with a linear type system grounded in Linear Logic and session types, ensuring resources and memory are never misused or leaked. It adopts a tutorial style to demonstrate session-based programming patterns, higher-order computation, and shared mutable state, all while maintaining strong correctness guarantees via type-checking. Key contributions include a suite of concrete examples—Hello World, basic and replicated session programming, lazy data structures, shared state, barriers, mutable queues, and a digital-assets ADT—that illustrate how the type system enforces safety properties automatically. The results suggest broad practical relevance for systems programming, with prototypes and ongoing work toward LLVM/CLANG backends and alignment with languages that already embrace linear or resource-aware typing.

Abstract

CLASS is a proof-of-concept general purpose linear programming language, flexibly supporting realistic concurrent programming idioms, and featuring an expressive linear type system ensuring that programs (1) never misuse or leak stateful resources or memory, (2) never deadlock, and (3) always terminate. The design of CLASS and the strong static guarantees of its type system originates in its Linear Logic and proposition-as-types foundations. However, instead of focusing on its theoretical foundations, this paper briefly illustrates, in a tutorial form, an identifiable CLASS session-based programming style where strong correctness properties are automatically ensured by type-checking. Our more challenging examples include concurrent thread and memory-safe mutable ADTs, lazy stream programming, and manipulation of linear digital assets as used in smart contracts.