Построение инстансов типа с разрешимым равенством. Метапрограммирование с каноническими структурами
Введение в формальную верификацию программ