Introduction ยง
Linear types are an application to type theory of the discipline of
linear logic, first described by Jean-Yves Girard
(Girard, 1987).
Since its inception it has led to many fruitful discoveries in
computer science. In this article I hope to explain why it is so
interesting, as well as relate it to concrete tools and practices
available to programmers today.
