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

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

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



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






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


Программные системы: теория и приложения, 2018, том 9, выпуск 4, страницы 509–560 (Mi ps327)  

Математические основы программирования

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

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

Институт программных систем им. А. К. Айламазяна РАН

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

Ключевые слова и фразы: компьютерная алгебра, арифметика двоичных кодов, доказательное программирование, язык Agda.

Финансовая поддержка Номер гранта
Российская академия наук - Федеральное агентство научных организаций AAAA-A16-116021760039-0
Исследование выполнено в рамках госзадания ФАНО России № г/р AAAA-A16-116021760039-0.


DOI: https://doi.org/10.25209/2079-3316-2018-9-4-509-560

Полный текст: PDF файл (2231 kB)
Список литературы: PDF файл   HTML файл

Тип публикации: Статья
УДК: 510.252, 004.432.42
MSC: Primary 03B35; Secondary 68T15, 03D60
Поступила в редакцию: 03.07.2018
19.12.2018
Подписана в печать : 30.12.2018

Образец цитирования: С. Д. Мешвелиани, “Построение доказательных программ арифметики натуральных чисел в двоичном представлении”, Программные системы: теория и приложения, 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}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/ps327
  • http://mi.mathnet.ru/rus/ps/v9/i4/p509

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Программные системы: теория и приложения
    Просмотров:
    Эта страница:38
    Полный текст:15
    Литература:4
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019