Построение доказательных программ арифметики натуральных чисел в двоичном представлении
Автор: Мешвелиани Сергей Давидович
Журнал: Программные системы: теория и приложения @programmnye-sistemy
Рубрика: Математические основы программирования
Статья в выпуске: 4 (39) т.9, 2018 года.
Бесплатный доступ
Поддержка зависимых типов в функциональном языке программирования Agda создаёт возможность включать в программу машинно-проверяемые доказательства. Рассмотрена задача доказательного включения алгоритмов арифметических действий над натуральными числами в двоичном представлении. Построена библиотека доказательных программ алгоритмов обычных письменных вычислений, действующих над списками двоичных разрядов чисел. Она содержит машинно-проверяемые доказательства необходимых свойств применённых алгоритмов, исправляет и существенно дополняет часть Bin стандартной библиотеки lib-0.16 языка Agda.
Арифметика двоичных кодов, доказательное программирование, компьютерная алгебра, язык agda
Короткий адрес: https://sciup.org/143166183
IDR: 143166183
Список литературы Построение доказательных программ арифметики натуральных чисел в двоичном представлении
- U. Norell. "Dependently typed programming in Agda", AFP 2008: Advanced Functional Programming, Lecture Notes in Computer Science, vol. 5832, Springer, Berlin-Heidelberg. P. 230-266.
- S. P. Jones. Haskell 98 Language and Libraries: The Revised Report, Cambridge University Press, 2003.
- A. Chlipala. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, MIT Press, 2013.
- А. А. Марков. О конструктивной математике//Проблемы конструктивного направления в математике. 2. Конструктивный математический анализ, Труды МИАН СССР, т. 67, М.-Л., 1962. С. 8-14.
- P. Martin-Löef. Intuitionistic type theory, Bibliopolis, 1984.
- W. A. Howard. "The formulae-as-types notion of construction", To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism., Academic Press, Boston, 1980. P. 479-490.
- H. B. Curry, R. Feys. Combinatory Logic. V. I, North-Holland, Amsterdam, 1958.
- А. А. Карацуба. Сложность вычислений//Оптимальное управление и дифференциальные уравнения, Сборник статей. К семидесятилетию со дня рождения академика Евгения Фроловича Мищенко, Тр. МИАН, т. 211, Наука, Физматлит, М., 1995. С. 186-202.
- N. Magaud. "Changing data representation within the Coq system", TPHOLs 2003: Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 2758, eds. D. Basin, B. Wolff, Springer, Berlin-Heidelberg, 2003. P. 87-102.
- С. Д. Мешвелиани. O зависимых типах и интуиционизме в программировании математики//Программные системы: теория и приложения, Т. 5, № 3. 2014. С. 27-50.
