TN
можно попробовать в эту штуку зайти с IR кодировок
Size: a a a
2017 December 21
TN
но вообще вся теория индуктивных типов — именно про это
TN
IR кодировки — это универсальная индукция
TN
хоттовские кодирвки еще есть, которые Андрей занимается, по статье ученика Эводи
TN
их не много всего 4-6 подходов для моделирования индуктивных типов
TN
вот кстати одна из последних IR кодировок
https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/variantsIR/
которая была на Types 2017
https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/variantsIR/
которая была на Types 2017
TN
CoC 88 да
TN
но рекурсоры и все остальное там актуальное
TN
а куб барендрехта немного устарел в контексте всех расширений зависимой теории
TN
а там ведь все типосистемы собраны куба
TN
этот пейпер 88 года это по сути дока по Ому :-)
TN
из (4) нам надо только SAR нотация
NK
я бы не сказал что "устарел", просто там всё системы без индукции, что в контексте верификации неинтересно
NK
т.е. просто не та тема
NK
Я реквестирую добавление в список талмуда Норстрома
NK
ЗП
если вы про то
2017 December 22
NK
запушил туда же rec_nat
NK
и ind_nat