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

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

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


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




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

Программные системы: теория и приложения, 2015, том 6, выпуск 4, страницы 313–340 (Mi ps190)  
Эта публикация цитируется в 1 научной статье (всего в 1 статье)

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

Программирование основ вычислительной алгебры на языке с зависимыми типами

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

Институт программных систем имени А. К. Айламазяна РАН
PDF полного текста (1593 kB) Список цитирования (1)
Список литературы:
PDF
HTML
Аннотация: В статье описываются главные черты разработанной автором на основе доказательного программирования библиотеки вычислительной алгебры. Обсуждается опыт доказательного программирования некоторых классических категорий вычислительной алгебры («группа», «кольцо» и так далее) на основе подхода конструктивизма, применения языка с зависимыми типами, построения машинно-проверяемых доказательств (dependent types, proof carrying code). Выявляются проблемы, связанные с этим подходом, и отмечаются дополнительные возможности, даваемые применением аппарата зависимых типов. В качестве инструмента используется функциональный язык Agda. Статья является продолжением вводной статьи автора в данном журнале за 2014 год.
Ключевые слова и фразы: конструктивная математика, алгебра, зависимые типы, функциональное программирование, Agda.
Финансовая поддержка Номер гранта
Российская академия наук - Федеральное агентство научных организаций г/р 01201354590
г/р 01201455360
Исследование выполнено в рамках НИР «Методы анализа и верификации моделей вычислительных систем и алгебраических объектов на основе средств функционального и логического программирования» (№ г/р 01201354590) и «Методы и средства разработки эффективного программного обеспечения, ориентированные на вычислительные системы, построенные на основе микропроцессоров с многоядерной архитектурой, и формальные основы высокоуровневых языков программирования для суперкомпьютеров с гибридной архитектурой» (№ г/р 01201455360) (госзадание ФАНО России).
Поступила в редакцию: 17.11.2015
Подписана в печать : 23.12.2015
Тип публикации: Статья
УДК: 510.252, 004.432.42
Образец цитирования: С. Д. Мешвелиани, “Программирование основ вычислительной алгебры на языке с зависимыми типами”, Программные системы: теория и приложения, 6:4 (2015), 313–340
Цитирование в формате AMSBIB
\RBibitem{Mec15}
\by С.~Д.~Мешвелиани
\paper Программирование основ вычислительной алгебры на языке с~зависимыми типами
\jour Программные системы: теория и приложения
\yr 2015
\vol 6
\issue 4
\pages 313--340
\mathnet{http://mi.mathnet.ru/ps190}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/ps190
  • https://www.mathnet.ru/rus/ps/v6/i4/p313
    • Эта публикация цитируется в следующих 1 статьяx:
    Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    		Программные системы: теория и приложения
    Статистика просмотров:
    Страница аннотации:355
    PDF полного текста:150
    Список литературы:69
     
      Обратная связь:
    		  Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024