О зависимых типах и интуиционизме в программировании математики
Автор: Мешвелиани Сергей Давидович
Журнал: Программные системы: теория и приложения @programmnye-sistemy
Рубрика: Математические основы программирования
Статья в выпуске: 3 (21) т.5, 2014 года.
Бесплатный доступ
Обсуждается практическая возможность доказуемого программирования математики на основе подхода конструктивизма и применения языка с зависимыми типами (dependent types, proof carrying code). Принципы конструктивизма и доказуемого программирования объясняются на примерах. Рассмотрение опирается на опыт реализации на языке \textsys{Agda} небольшой библиотеки вычислительной алгебры, включающей арифметику области остатков $R/(b)$ для евклидова кольца $R$.
Алгебра, зависимые типы, конструктивная математика
Короткий адрес: https://sciup.org/14335983
IDR: 14335983
Список литературы О зависимых типах и интуиционизме в программировании математики
- Haskell 2010: A Non-strict, Purely Functional Language. Report of 2010. Home page of the Haskell materials, URL http://www.haskell.org.
- S. D. Mechveliani. Computer algebra with Haskell: applying functionalcategorial-‘lazy’ programming//International Workshop CAAP-2001. -Dubna, Russia, 2001, p. 203-211., URL http://compalg.jinr.ru/Confs/CAAP_ 2001/Final/proceedings/proceed.pdf.
- U. Norell, J. Chapman. Dependently Typed Programming in Agda, URL http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf.
- S. D. Meshveliani. Dependent Types for an Adequate Programming of Algebra // Electronic Journal CEUR Workshop Proceedings // Intelligent Computer Mathematics. CICM-WS-WiP 2013, Workshops and Work in Progress at CICM. – Bath, UK, 2013. – Vol. 1010., URL http: //ceur-ws.org/Vol-1010/paper-05.pdf.
- S. D. Meshveliani. Experience in an Adequate Programming of Algebra in a Language with Dependent Types//Polynomial Computer Algebra 2014. Extended Abstracts. -St. Petersburg: VVM Publishing, St. Petersburg, 2014, -p. 54-57.
- А. И. Кострикин. Введение в алгебру. Основы алгебры. М.: Наука. Физматлит, 1994.
- Дж. Коллинз, Р. Лоос. Компьютерная алгебра. Символьные и алгебраические вычисления/ред. Б. Бухбергер. М.: Мир, 1986.
- Дж. Давенпорт, И. Сирэ, Э. Турнье. Компьютерная алгебра. М.: Мир, 1991.
- R. D. Jenks, R. S. Sutor et al. Axiom, the Scientific Computation System. New York-Heidelberg-Berlin: Springer-Verlag, 1992.
- S. Watt et al. Aldor Compiler User Guide. IBM Thomas J. Watson Research Center, URL http://www.aldor.org.
- The Coq Proof Assistant. Homepage of the Coq system, URL http://coq.inria.fr.
- Agda. A dependently typed functional programming language and its system. Homepage of Agda, URL http://wiki.portal.chalmers.se/agda/pmwiki.php.
- А. А. Марков. О конструктивной математике//Проблемы конструктивного направления в математике. 2. Конструктивный математический анализ. Труды МИАН СССР. -М.-Л., 1962. Т. 67, c. 8-14., URL http://mi.mathnet.ru/tm1756.
- P. Martin-L¨ef. Intuitionistic Type Theory: Bibliopolis, 1984.
- G. Higman. Ordering by divisibility in abstract algebras//Proceedings of the London Mathematical Society, 1952. Vol. s3-2, no. 1, p. 326-336.
- S. Berghofer. A constructive proof of Higman’s lemma in Isabelle//Types for Proofs and Programs, International Workshop (TYPES 2003). LNCS/S. Berardi, M. Coppo (eds.): Springer-Verlag, 2004. Vol. 3085, p. 66-82.
- S. Romanenko. A proof in Agda of Higman’s lemma., URL https://github.com/sergei-romanenko/agda-miscellanea/tree/master/Higman.
- P. Kokke, W. Swierstra. Auto in Agda: Programming proof search, 2014, URL http://www.staff.science.uu.nl/~swier004/Publications/AutoInAgda.pdf., Under preparation for ICFP 2014.
- A. Mahboubi. The Rooster and the Butterflies//Intelligent Computer Mathematics. LNAI. -Berlin-Heidelberg: Springer-Verlag, 2013. Vol. 7961, -p. 1-18.
