Linear logic is often introduced with unintuitive and contrived examples involving food. For computer scientists, linear logic is well motivated by memory management à la C.

In typical compiled languages, code is static and values are heap- or stack-allocated. Management of stack-allocated values is left to the compiler.

Heap-allocated values begin with malloc and end with free. Linear logic requires that all values be consumed exactly once (motto: every question must have an answer and every answer a question); one must free a value and it can be freed only once. Thus, memory is not leaked and we do not have double-free errors.

• $$A$$ - the type of a heap-allocated value
• $$A \oplus B$$ - a sum type
• $$A \otimes B$$ - a strict pair, a product type. A tuple or a struct in C (for instance).
• $$!A$$ - the type of a stack-allocated value (or the type of a static immutable value)
• $$A \multimap B$$ - $$A \multimap B$$ comes up in currying and application. We can use the conventional arrow $$A \rightarrow B$$ to denote "B is a consequent of A"; in this context it means we have a function to compute B from A.

If we have an uncurried function $$A \otimes B \rightarrow C$$, we can curry to get $$A \rightarrow B \multimap C$$. Curried functions can be applied, $${\tt apply} : (A \multimap B) \otimes A \rightarrow B$$.

This makes sense: a partially applied function might be returned as a closure. This closure would reference $$A$$ but $$A$$ would not be consumed until the function was called. One might leak space if such functions were taken to be like the static procedures that are compiled.

For a standard C program:

int main(void);

In linear logic, the type of main would be 𝟙 → !Int. Some more examples:

void free(void *ptr);

VoidPtr → 𝟙

void *malloc(size_t size);

!Size → VoidPtr

void *realloc(void *ptr, size_t size);

(VoidPtr ⊗ !Size) → VoidPtr