Утверждения как сессии

Классическое соответствие Карри-Говарда между интуиционистской логикой и просто типизированным лямбда-исчислением наталкивает на мысль, что это соответствие продолжается как на более сложные логики, так и на более интересные диалекты лямбда-исчисления. В частности, для интуиционистской линейной логики с экспоненциалом ! нетрудно выписать соответствующий субструктурный вариант лямбда-исчисления; полученный язык наделяет линейные типы "ресурсной" семантикой. Однако более естественной "логикой ресурсов" оказывается т.н. uniqueness logic [Harrington 2006], в то время как реализации линейных систем менее эффективны.
Оказывается, что у собственно линейной логики есть совершенно другая интерпретация — утверждений как сессий, в которых утверждения описывают некоторый протокол взаимодействия (сессию); соответствующим исчислением, позволяющим описывать "процессы", удовлетворяющие протоколам, оказывается π-исчисление, формализм для описания параллельных процессов.
В предлагаемом слушателям докладе будут изложены наиболее успешные результаты по реализации программы утверждений как сессий по мотивам статей Propositions as Sessions [Wadler 2014], Better late than never и Taking Linear Logic Apart [Kokke 2019].