Теория типов, компьютерная алгебра, поддержка доказательств и грамматики

Теория типов, компьютерная алгебра, поддержка доказательств и грамматики

Автор: Федорченко Людмила Николаевна

Журнал: Вестник Бурятского государственного университета. Математика, информатика @vestnik-bsu-maths

Рубрика: Информационные системы и технологии

Статья в выпуске: 2, 2016 года.

Бесплатный доступ

Данная статья посвящена краткому обзору и рассмотрению основных направлений исследований, связанных с теорией типов и её приложениями. Даётся характеристика универсальных систем аналитических вычислений (систем компьютерной алгебры), а также систем поддержки аналитических вычислений и возможных доказательств истинности выводов (Proof Assistants). Рассмотрено применение типов в современной информатике, прежде всего, в функциональном и объектно-ориентированном программировании. Перечислены основные научные коллективы, ведущие исследования и разработки программных систем в данном направлении.

Типы, подтипы, формальные системы, системы поддержки доказательств, трансформации на графах, грамматики

Короткий адрес: https://sciup.org/14835180

IDR: 14835180   |   DOI: 10.18101/2304-5728-2016-2-55-76

Список литературы Теория типов, компьютерная алгебра, поддержка доказательств и грамматики

  • Шанин H.A. Доклад на IV Всесоюзном математическом съезде в июне 1961 г.
  • Whitehead, Alfred North, and Bertrand Russell (1910, 1912, 1913) Principia Mathematica, 3 vols, Cambridge: Cambridge University Press. Second edition, 1925 (Vol. 1), 1927 (Vols 2, 3). Abridged as Principia Mathematica to *56, Cambridge: Cambridge University Press, 1962.
  • Godel K. On intuitionistic arithmetic and number theory. In M. Davis (Ed.) The Undecidable. Raven Press. N.Y., 1965.
  • Martin-Lof P. Intuitionistic type theory. Bibliopolis, 1984.
  • Coquand T., Huet G. Constructions: a higher order proof system for machanized mathematics. Proc. 1985 European Conference on Computer Algebra, Lecture Notes in Computer Science. V. 203. Springer, 1985.
  • Barendregt H., Barendsen E. “Autarkic computations in formal proofs“. Journal of Automated Reasoning, 28(3). 2002. P. 321 -336.
  • Bronstein M. “Computer Algebra Algorithms for Linear Ordinary Differential and Difference Equations”. Preprint INRIA. 2001.
  • Barendregt H., (with Cohen A.) “Electronic Communication of Mathematics and the Interaction of Computer Algebras Systems and Proof Assistants” J. Symbolic Computation, 32 (2001). P. 3 -22.
  • Barendregt H. (with Geuvers H.) Proof-checking using Dependent Type Systems. Handbook of Artificial Reasoning. Vol.II. Ch.18 (2001). 1149-1240.
  • Ranta A. Grammatical Framework: A Type-Theoretical Grammar Formalism. Manuscript, September 2002. Journal of Functional Programming, to appear.
  • Ranta A. Type-theoretical interpretation and generalization of phrase structure grammar. Bulletin of the IGPL 3. 1995. P. 319 -342.
  • Hallgren T. and Ranta A. "An Extensible Proof Text Editor". M. Parigot & A. Voronkov (eds), Logic for Programming and Automated Reasoning (LPAR'2000), LNCS/LNAI. 1955. P. 70 -84, Springer Verlag, Heidelberg, 2000.
  • Ranta A. A Multilingual Natural-Language Interface to Regular Expressions, L. Karttunen and K. Oflazer (eds). Proceedings of the International Workshop on Finite State Methods in Natural Language Processing, Bilkent University, Ankara, 1998. P. 79 -90.
  • Coquand T. Domain Models in Type Theory. URL: (Slides: http://www.cs.chalmers.se/~coquand/type.html).
  • Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на C++. -Изд-во Бином, 1998. -560 с.
  • De Bruijn, N.G. A survey of the project AUTOMATH. In: Seldin, J.P. and Hindley, J.R. Eds. To H.B. Curry:Essays in Combinatory Logic, Lambda Calculus and Formalism. (1980). Academic Press. P. 589-606.
  • Gordon М., Milner R. and Wadsworth C. Edinburgh LCF: A Mechanized Logic of Computation. Lect. Notes in Comp. Sei, V. 78. 1979.
  • Paulson L. Interactive Theorem Proving with Cambridge LCF. Tech. rep. 80, Computer Laboratory, Univ. of Cambridge, Nov. 1985.
  • Petersson K. A programming system for type theory. Tech. Rep.21, Programming Methodology Group, Univ. of Gotheborg/Chalmers Institute of Technology. Mar. 1982.
  • Coquand T., Huet G. Constructions: A higher-order proof system for machanized mathematics. In: EUROCAl'85: European Conference on Computer Algebra (1985), B. Buchberger, Ed., Vol. 203 of Lecture Notes in Computer Science, Spinger. P. 151 -184.
  • Constable R. L. et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986.
  • Luo Z. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Oxford, 1994.
  • Luo Z. PAL+: A lambda-free logical framework. J. Functional Programming, 2001.
  • Luo Z., Pollack R. Lego Proof Developmnet System: user's manual, LFCS Report ECS-LFCS-92-211, department of computer science, University of Edinburgh.
  • Callaghan P. and Luo Z. Plastic: an implementation of typed LF with coercive subtyping and universes. Submitted to Proc. LFM'99, 2000.
  • Soloviev S., Luo Z. Coercion Completion and Conservativity in Coercive Subtyping. Annals of Pure and Applied Logic. 113 (2002). 297 -322.
  • McBride C. Faking It: Simulating Dependent Types in Haskell. J.
  • Callaghan P. C. An Evaluation of LOLITA and Related Natural Language Processing Systems. PhD thesis, University of Durham, Department of Computer Science, Laboratory for Natural Language Engineering, 1997.
  • Coquand T. and Huet G. The calculus of constructions. Information and Computation, 76(2/3):95-120. February/March 1988.
  • Saibi A. and Huet G. "Constructive Category Theory" In Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory, Goteborg (Sweden), January 95.
  • Матулис В. А. Первый всесоюзный симпозиум по проблеме машинного поиска логического вывода. -Успехи мат. наук. -T. XIX, вып. 6. -1964. -С. 239 -241.
  • Шанин Н. А., Давыдов Г. В., Маслов С. Ю., Минц Г.E., Оревков B.П., Слисенко А. О. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний. -«Наука», 1965. -39 с. .
  • Маслов С. Ю. Обратный метод установления выводимости в классическом исчислении предикатов. -Докл. АН СССР. -Т. 159, №.1. -1964,-С. 17-20.
  • Давыдов Г. В., Маслов С. Ю., Минц Г.E., Оревков В.П., Слисенко А. О. Машинный алгорифм установления выводимости на основе о обратного метода. -Зап. научн. семинаров ЛОМИ. -1969. -Т.16. -C. 8-19.
  • Niqui М. Constructive Reals in Coq: Axioms and First Order Equivalence, Types 2000 Workshop, December 7-12 2000. Univ. of Durham.
  • Capprotti O., Oostdijk M. Formal and effective primality proofs by use of Computer Algebra Oracles. JSC, Special Issue on Computer Algebra and Mechanized Reasoning, 2001.
  • Carpetta V. Certifying Fast Fourier Transform with Coq. Manuscript.
  • Frank Pfenning and Carsten Schermann. System description: Twelf -a meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), Trento, Italy, July 1999. Springer-Verlag LNAI 1632. P. 202 -206.
  • Соловьев C.B. Категория конечных множеств и декартово замкнутые категории. -Зап. Научных семинаров ЛОМИ. -1981. -Т. 105. -С. 174-194.
  • Di Cosmo R. Isomorphism of Types. Burkhauser, 1995.
  • Chemouil D., Soloviev S. Extensional Isomorphisms of Inductive Types in Simply Typed Lambda-calculus. -15 p. Submitted.
  • Федорченко Л. H., Соловьев С. В. Синтаксические преобразования в системе SynGT и их новые приложения//Материалы VIII Санкт-Петербургской международной конференции «Региональная информатика-2002». -Ч. 2. -СПб: СПОИСУ, 2002. -С. 50.
  • Fedorchenko L. N., Soloviev S. V., Naumov I. N., Mehats L. Syntax Graph Transformations in the System SynGT and their Applications. -Rapport IRIT/2003-06-R. UMR 5505 CNRS-INP-UPS. 15 pp. (English).
  • Fedorchenko L. and Baranov S. Equivalent Transformations and Regularization in Context-Free Grammars. Bulgarian Academy of Sciences. Cybernetics and Information Technologies (CIT). Vol. 14. No. 4. P. 11-28. Sofia 2015 (Scopus).
  • Федорченко Л. H. SynGT: применение атрибутов//Региональная информатика и информационная безопасность. -Сб. трудов. -Вып. 1. -СПб.: СПОИСУ, 2015. -С. 68 -73.
  • Boisvert В., Feraud L., Soloviev S. Typed lambda terms in categorical graph rewriting//In The International Conference Polynomial Computer Algebra, April 18-22, 2011. Saint-Petersburg, Russia, Euler International Mathematical Institute. VVM Publishing. P. 9 -16.
  • Баранов C. H., Буавер Б., Соловьев С. В., Феро Л. Некоторые приложения лямбда-исчислений с типами к атрибутным вычислениям в системах категорных преобразований графов//Труды СПИИРАН. -2012. -Вып. 23. -С. 296 -323.
Еще
Статья научная
SciUp 2024 © 2024 ©