Аннотация:
Поддержка зависимых типов в функциональном языке программирования Agda создаёт
возможность включать в программу машинно-проверяемые доказательства. Рассмотрена задача доказательного
включения алгоритмов арифметических действий над натуральными числами в двоичном представлении.
Построена библиотека доказательных программ алгоритмов обычных письменных вычислений, действующих над
списками двоичных разрядов чисел. Она содержит машинно-проверяемые доказательства необходимых свойств
применённых алгоритмов, исправляет и существенно дополняет часть Bin стандартной библиотеки
lib-0.16 языка Agda.
Ключевые слова и фразы:компьютерная алгебра, арифметика двоичных кодов, доказательное программирование, язык Agda.