Линейная логика и функциональное программирование

Линейная логика (Жирар, 1987) — это система, в которой логические формулы воспринимаются не как высказывания, а как ресурсы, которые разрешается использовать ровно один раз. В связи с этим в линейной логике отсутствуют обыкновенные для логики классической правила сокращения (ресурс $A$ нельзя заменить на две его копии, $A$ и $A$) и ослабления (каждый ресурс должен быть использован). При этом в линейной логике есть механизм, позволяющий восстанавливать эти правила в ограниченном виде и тем самым моделировать классические рассуждения. Интерес к логическим системам со стороны функционального программирования основан на изоморфизме Карри – Говарда: выражение $A \to B$ можно понимать и как логическую операцию импликации, и как обозначение для типа функций из $A$ в $B$. Обыкновенным системам типов, применяемым в функциональных языках, по Карри – Говарду соответствует интуиционистская логика. Если, однако, заменить её на линейную, то система типов обогатится новыми возможностями — в частности, синтаксическим механизмом отслеживания того факта, что данный объект используется в данный момент ровно одним процессом в многопоточной среде.