Программные системы: теория и приложения
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Общая информация
Последний выпуск
Архив
Правила для авторов
Загрузить рукопись

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS


Программные системы: теория и приложения:
Год:
Том:
Выпуск:
Страница:
Найти




Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация

Программные системы: теория и приложения, 2018, том 9, выпуск 4, страницы 509–560
DOI: https://doi.org/10.25209/2079-3316-2018-9-4-509-560 (Mi ps327) 		 
Математические основы программирования

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

С. Д. Мешвелиани

Институт программных систем им. А. К. Айламазяна РАН
PDF полного текста (2231 kB)
Список литературы:
PDF
HTML
DOI: https://doi.org/10.25209/2079-3316-2018-9-4-509-560
Аннотация: Поддержка зависимых типов в функциональном языке программирования Agda создаёт возможность включать в программу машинно-проверяемые доказательства. Рассмотрена задача доказательного включения алгоритмов арифметических действий над натуральными числами в двоичном представлении.
Построена библиотека доказательных программ алгоритмов обычных письменных вычислений, действующих над списками двоичных разрядов чисел. Она содержит машинно-проверяемые доказательства необходимых свойств применённых алгоритмов, исправляет и существенно дополняет часть Bin стандартной библиотеки lib-0.16 языка Agda.
Ключевые слова и фразы: компьютерная алгебра, арифметика двоичных кодов, доказательное программирование, язык Agda.
Финансовая поддержка Номер гранта
Российская академия наук - Федеральное агентство научных организаций AAAA-A16-116021760039-0
Исследование выполнено в рамках госзадания ФАНО России № г/р AAAA-A16-116021760039-0.
Поступила в редакцию: 03.07.2018
19.12.2018
Подписана в печать : 30.12.2018
Тип публикации: Статья
УДК: 510.252, 004.432.42
MSC: Primary 03B35; Secondary 68T15, 03D60
Образец цитирования: С. Д. Мешвелиани, “Построение доказательных программ арифметики натуральных чисел в двоичном представлении”, Программные системы: теория и приложения, 9:4 (2018), 509–560
Цитирование в формате AMSBIB
\RBibitem{Mec18}
\by С.~Д.~Мешвелиани
\paper Построение доказательных программ арифметики натуральных чисел в двоичном представлении
\jour Программные системы: теория и приложения
\yr 2018
\vol 9
\issue 4
\pages 509--560
\mathnet{http://mi.mathnet.ru/ps327}
\crossref{https://doi.org/10.25209/2079-3316-2018-9-4-509-560}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/ps327
  • https://www.mathnet.ru/rus/ps/v9/i4/p509
    • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    		Программные системы: теория и приложения
    Статистика просмотров:
    Страница аннотации:177
    PDF полного текста:236
    Список литературы:23
     
      Обратная связь:
    		  Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024