| RUS ENG |
| Полная версия |
|
|
|
| СЕМИНАРЫ |
|
Рабочий семинар по математической логике
|
|||
|
|
|||
|
Утверждения как сессии П. П. Соколов |
|||
|
Аннотация: Классическое соответствие Карри–Говарда между интуиционистской логикой и просто типизированным лямбда-исчислением наталкивает на мысль, что это соответствие продолжается как на более сложные логики, так и на более интересные диалекты лямбда-исчисления. В частности, для интуиционистской линейной логики с экспоненциалом ! нетрудно выписать соответствующий субструктурный вариант лямбда-исчисления; полученный язык наделяет линейные типы "ресурсной" семантикой. Однако более естественной "логикой ресурсов" оказывается так называемая uniqueness logic [Harrington 2006], в то время как реализации линейных систем менее эффективны. Оказывается, что у собственно линейной логики есть совершенно другая интерпретация — утверждений как сессий, в которых утверждения описывают некоторый протокол взаимодействия (сессию); соответствующим исчислением, позволяющим описывать "процессы", удовлетворяющие протоколам, оказывается π-исчисление, формализм для описания параллельных процессов. В предлагаемом слушателям докладе будут изложены наиболее успешные результаты по реализации программы утверждений как сессий по мотивам статей "Propositions as sessions" [Wadler 2014], "Better late than never" и "Taking linear logic apart" [Kokke 2019]. |
|||
