Построение доказательных программ арифметики натуральных чисел в двоичном представлении

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