##2018
##2017
Сергей Романенко. Доказательства методом бесконечного спуска и их формализация на Агде. Май 2017. PDF
Сергей Романенко. Доказательство леммы Хигмана (для двух букв) формализованное на Агде. Июль 2017. PDF MD
Сергей Романенко. Рефал и Агда как воплощения идеи “метаалгоритмического языка”. Сентябрь 2017. PDF Agda code
##2011
##2009