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.

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