Skip to main content

Questions tagged [substructural-types]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
11 votes
1 answer

What is "graded modality" in type theory?

I'm referring to these papers: Graded Modal Dependent Type Theory (The Gerty Language) Quantitative program reasoning with graded modal types (The Granule Language) At first glance, it seems graded ...
tarzh's user avatar
  • 3,914
9 votes
1 answer

Why does ATTAPL's linear product introduction rule not delete the objects from the context?

In Chapter 1 of Advanced Topics in Types and Programming Languages, the following rule is presented for the introduction of a product in a linear/unrestricted type system: ($\circ$ is context ...
blueberry's user avatar
  • 2,455
12 votes
2 answers

How do linear types interact with features that may change the normal control flow?

Linear types are quite a powerful feature of type systems that ensure that "linear values" are used exactly once. For example, ...
Luiz Felipe's user avatar