Substructural type system

Substructural type systems are a family of type systems analogous to substructural logics where one or more of the structural rules are absent or only allowed under controlled circumstances. Such systems are useful for constraining access to system resources such as , locks, and memory by keeping track of changes of state that occur and preventing invalid states. Several type systems have emerged by discarding some of the structural rules of exchange, weakening, and contraction: Ordered type systems (discard exchange, weakening and contraction): Every variable is used exactly once in the order it was introduced. Linear type systems (allow exchange, but neither weakening nor contraction): Every variable is used exactly once. Affine type systems (allow exchange and weakening, but not contraction): Every variable is used at most once. Relevant type systems (allow exchange and contraction, but not weakening): Every variable is used at least once. Normal type systems (allow exchange, weakening and contraction): Every variable may be used arbitrarily. The explanation for affine type systems is best understood if rephrased as “every occurrence of a variable is used at most once”. Ordered types correspond to noncommutative logic where exchange, contraction and weakening are discarded. This can be used to model stack-based memory allocation (contrast with linear types which can be used to model heap-based memory allocation). Without the exchange property, an object may only be used when at the top of the modelled stack, after which it is popped off, resulting in every variable being used exactly once in the order it was introduced. Linear types corresponds to linear logic and ensures that objects are used exactly once. This allows the system to safely deallocate an object after its use, or to design software interfaces that guarantee a resource cannot be used once it has been closed or transitioned to a different state. The Clean programming language makes use of uniqueness types (a variant of linear types) to help support concurrency, input/output, and in-place update of arrays.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (9)

Related courses (4)

CS-628: Interactive Theorem Proving CS

A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code!

CS-452: Foundations of software

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a progr

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language in

Related lectures (39)

Uniqueness type

In computing, a unique type guarantees that an object is used in a single-threaded way, with at most a single reference to it. If a value has a unique type, a function applied to it can be optimized to update the value in-place in the object code. Such in-place updates improve the efficiency of functional languages while maintaining referential transparency. Unique types can also be used to integrate functional and imperative programming. Uniqueness typing is best explained using an example.

Rust (programming language)

Rust is a multi-paradigm, general-purpose programming language that emphasizes performance, type safety, and concurrency. It enforces memory safety—ensuring that all references point to valid memory—without requiring the use of a garbage collector or reference counting present in other memory-safe languages. To simultaneously enforce memory safety and prevent data races, its "borrow checker" tracks the object lifetime of all references in a program during compilation.

Linear logic

Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics (because linear logic can be seen as the logic of quantum information theory), as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction.

Designing Formally Correct Intermittent Systems

Explores designing formally correct intermittent systems for extreme edge computing platforms, emphasizing correctness, reliability, and security.

Foundations of Software: Modeling Programming Languages CS-452: Foundations of software

Covers the mathematical study of program behaviors, parsing, domain-specific languages, and powerful tools for language design.

Taming Null References CS-550: Formal verification

Explores the challenges of null references in programming languages and proposes solutions to mitigate their drawbacks while ensuring compatibility with existing codebases.