Хорошее введение в Calculus of Constructions

Наверняка многие из вас слышали про языки с зависимыми типами. Кто-то смотрел примеры кода на Agda и Idris2, а кто-то, возможно, даже отложил себе в закладки замечательные книги серии Software Foundations, описывающие тонкости применения Coq (и все никак не может начать их осваивать, да :)).

Авторам канала всегда нравилось разбираться в деталях технологий: территория неизвестного и непонятного манит и требует решительных действий! Как можно пользоваться инструментом, если не понимаешь, как он устроен внутри, хотя бы приблизительно?!

Пытаясь разобраться в особенностях calculus of constructions, мы наткнулись на великолепный документ, описывающий эту теорию типов с самых азов. В тексте даются все необходимые пререквизиты и вводятся базовые обозначения, которые понадобятся для погружения в мир CoC. Этим «Typed Lambda Calculus / Calculus of Constructions» значительно отличается от других подобных работ, требующих от читателя немалого багажа и погруженности в предмет.

Если вы заняты в сфере, где safety — важный quality-атрибут, самое время обратить внимание на мир языков с зависимыми типами. С каждым годом эти инструменты будут все популярнее.

#digest