Исправление SZT, (текущая версия) :
Вот кстати https://arxiv.org/pdf/1809.06336.pdf : Verification of High-Level Transformations with Inductive Refinement Types
Исходная версия SZT, :
Вот кстати https://arxiv.org/pdf/1809.06336.pdf : Verification of High-Level Transformations withInductive Refinement Types