Вестник БГУ. Математика, информатика
Библиографическое описание:
Теория типов, компьютерная алгебра, поддержка доказательств и грамматики // Вестник БГУ. Математика, информатика. - 2016. №2. . - С. 55-76.
Заглавие:
Теория типов, компьютерная алгебра, поддержка доказательств и грамматики
Финансирование:
Коды:
Аннотация:
Данная статья посвящена краткому обзору и рассмотрению основных направлений исследований, связанных с теорией типов и её приложениями. Даётся характеристика универсальных систем аналитических вычислений (систем компьютерной алгебры), а также систем поддержки аналитических вычислений и возможных доказательств истинности выводов (Proof Assistants). Рассмотрено применение типов в современной информатике, прежде всего, в функциональном и объектно-ориентированном программировании. Перечислены основные научные коллективы, ведущие исследования и разработки программных систем в данном направлении.
Ключевые слова:
типы, подтипы, формальные системы, системы поддержки доказательств, трансформации на графах, грамматики.
Список литературы:
1. Шанин Н.А. Доклад на IV Всесоюзном математическом съезде в июне 1961 г.
2. 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.
3. Godel K. On intuitionistic arithmetic and number theory. In M. Davis (Ed.) The Undecidable. Raven Press. N.Y., 1965.
4. Martin-Lof P. Intuitionistic type theory. Bibliopolis, 1984.
5. Coquand T., Huet G. Constructions: a higher order proof system for machanized mathematics. Proc. 1985 European Conference on Computer Al- gebra, Lecture Notes in Computer Science. V. 203. Springer, 1985.
6. Barendregt H., Barendsen E. “Autarkic computations in formal proofs“. Journal of Automated Reasoning, 28(3). 2002. P. 321 – 336.
7. Bronstein M. “Computer Algebra Algorithms for Linear Ordinary Dif- ferential and Difference Equations”. Preprint INRIA. 2001.
8. Barendregt H., (with Cohen A.) “Electronic Communication of Mathe- matics and the Interaction of Computer Algebras Systems and Proof Assis- tants” J. Symbolic Computation, 32 (2001). P. 3 – 22.
9. Barendregt H. (with Geuvers H.) Proof-checking using Dependent Type Systems. Handbook of Artificial Reasoning. Vol.II. Ch.18 (2001). 1149–1240.
10. Ranta A. Grammatical Framework: A Type-Theoretical Grammar Formalism. Manuscript, September 2002. Journal of Functional Programming, to appear.
11. Ranta A. Type-theoretical interpretation and generalization of phrase structure grammar. Bulletin of the IGPL 3. 1995. P. 319 – 342.
12. Hallgren T. and Ranta A. "An Extensible Proof Text Editor". M. Parigot & A. Voronkov (eds), Logic for Programming and Automated Reason ing (LPAR'2000), LNCS/LNAI. 1955. P. 70 – 84, Springer Verlag, Heidelberg, 2000.
13. 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.
14. Coquand T. Domain Models in Type Theory. URL: (Slides: http://www.cs.chalmers.se/~coquand/type.html).
15. Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на С++. — Изд-во Бином, 1998. — 560 с.
16. 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.
17. Gordon M., Milner R. and Wadsworth C. Edinburgh LCF: A Mechanized Logic of Computation. Lect. Notes in Comp. Sci, V. 78. 1979.
18. Paulson L. Interactive Theorem Proving with Cambridge LCF. Tech. rep. 80, Computer Laboratory, Univ. of Cambridge, Nov. 1985.
19. Petersson K. A programming system for type theory. Tech. Rep.21, Programming Methodology Group, Univ. of Gotheborg / Chalmers Institute of Technology. Mar. 1982.
20. Coquand T., Huet G. Constructions: A higher-order proof system for machanized mathematics. In: EUROCAl'85: European Conference on Com- puter Algebra (1985), B. Buchberger, Ed., Vol. 203 of Lecture Notes in Com- puter Science, Spinger. P.151 – 184.
21. Constable R. L. et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986.
22. Luo Z. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Oxford, 1994.
23. Luo Z. PAL+: A lambda-free logical framework. J. Functional Programming, 2001.
24. Luo Z., Pollack R. Lego Proof Developmnet System: user's manual, LFCS Report ECS–LFCS–92–211, department of computer science, University of Edinburgh.
25. Callaghan P. and Luo Z. Plastic: an implementation of typed LF with coercive subtyping and universes. Submitted to Proc. LFM'99, 2000.
26. Soloviev S., Luo Z. Coercion Completion and Conservativity in Coercive Subtyping. Annals of Pure and Applied Logic. 113 (2002). 297 – 322.
27. McBride C. Faking It: Simulating Dependent Types in Haskell. J.
28. 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.
29. Coquand T. and Huet G. The calculus of constructions. Information and Computation , 76(2/3):95–120. February/March 1988.
30. 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.
31. Матулис В. А. Первый всесоюзный симпозиум по проблеме машинного поиска логического вывода. — Успехи мат. наук. — T. XIX, вып. 6. — 1964. — С. 239 – 241.
32. Шанин Н. А., Давыдов Г. В., Маслов С. Ю., Минц Г.Е., Оревков В.П., Слисенко А. О. Алгорифм машинного поиска естественного логиче- ского вывода в исчислении высказываний. — «Наука», 1965. — 39 с. [in: Automation of reasoning, Springer-Verlag, Berlin. Vol.1. P. 424 – 483, 1983].
33. Маслов С. Ю. Обратный метод установления выводимости в классическом исчислении предикатов. — Докл. АН СССР. — Т.159, №.1. — 1964. — С. 17 – 20.
34. Давыдов Г. В., Маслов С. Ю., Минц Г.Е., Оревков В.П., Слисенко А. О. Машинный алгорифм установления выводимости на основе о об- ратного метода. — Зап. научн. семинаров ЛОМИ. — 1969. — Т .16. — С. 8 – 19.
35. Niqui M. Constructive Reals in Coq: Axioms and First Order Equiva-
lence, Types 2000 Workshop, December 7–12 2000. Univ. of Durham.
36. 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.
37. Carpetta V. Certifying Fast Fourier Transform with Coq. Manuscript.
38. Frank Pfenning and Carsten Schermann. System description: Twelf - a meta-logical framework for deductive systems. In H. Ganzinger, editor, Pro- ceedings of the 16th International Conference on Automated Deduction (CADE-16), Trento, Italy, July 1999. Springer-Verlag LNAI 1632. P. 202 –
206.
39. Соловьев С.В. Категория конечных множеств и декартово замкну- тые категории. — Зап. Научных семинаров ЛОМИ. — 1981. — Т. 105. — С. 174 – 194.
40. Di Cosmo R. Isomorphism of Types. Burkhauser, 1995.
41. Chemouil D., Soloviev S. Extensional Isomorphisms of Inductive Types in Simply Typed Lambda-calculus. — 15 p. Submitted.
42. Федорченко Л. Н., Соловьев С. В. Cинтаксические преобразования
в системе SynGT и их новые приложения // Материалы VIII Санкт- Петербургской международной конференции «Региональная информати- ка–2002». — Ч. 2. — СПб: СПОИСУ, 2002. — С. 50.
43. Fedorchenko L. N., Soloviev S. V., Naumov I. N., Mehats L. Syntax Graph Transformations in the System SynGT and their Applications. — Rap- port IRIT/2003-06-R. UMR 5505 CNRS-INP-UPS. 15 pp. (English).
44. Fedorchenko L. and Baranov S. Equivalent Transformations and Regu-
larization in Context–Free Grammars. Bulgarian Academy of Sciences. Cyber- netics and Information Technologies (CIT). Vol. 14. No. 4. P. 11–28. Sofia 2015 (Scopus).
45. Федорченко Л. Н. SynGT: применение атрибутов // Региональная информатика и информационная безопасность. — Сб. трудов. — Вып. 1. — СПб.: СПОИСУ, 2015. — С. 68 – 73.
46. Boisvert B., Feraud L., Soloviev S. Typed lambda terms in categorical graph rewriting // In The International Conference Polynomial Computer Alge- bra, April 18-22, 2011. Saint-Petersburg, Russia, Euler International Mathe- matical Institute.VVM Publishing. P. 9 – 16.
47. Баранов С. Н., Буавер Б., Соловьев С. В., Феро Л. Некоторые при-
ложения лямбда-исчислений с типами к атрибутным вычислениям в сис-
темах категорных преобразований графов // Труды СПИИРАН. —
2012. — Вып. 23. — С. 296 – 323.
2. 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.
3. Godel K. On intuitionistic arithmetic and number theory. In M. Davis (Ed.) The Undecidable. Raven Press. N.Y., 1965.
4. Martin-Lof P. Intuitionistic type theory. Bibliopolis, 1984.
5. Coquand T., Huet G. Constructions: a higher order proof system for machanized mathematics. Proc. 1985 European Conference on Computer Al- gebra, Lecture Notes in Computer Science. V. 203. Springer, 1985.
6. Barendregt H., Barendsen E. “Autarkic computations in formal proofs“. Journal of Automated Reasoning, 28(3). 2002. P. 321 – 336.
7. Bronstein M. “Computer Algebra Algorithms for Linear Ordinary Dif- ferential and Difference Equations”. Preprint INRIA. 2001.
8. Barendregt H., (with Cohen A.) “Electronic Communication of Mathe- matics and the Interaction of Computer Algebras Systems and Proof Assis- tants” J. Symbolic Computation, 32 (2001). P. 3 – 22.
9. Barendregt H. (with Geuvers H.) Proof-checking using Dependent Type Systems. Handbook of Artificial Reasoning. Vol.II. Ch.18 (2001). 1149–1240.
10. Ranta A. Grammatical Framework: A Type-Theoretical Grammar Formalism. Manuscript, September 2002. Journal of Functional Programming, to appear.
11. Ranta A. Type-theoretical interpretation and generalization of phrase structure grammar. Bulletin of the IGPL 3. 1995. P. 319 – 342.
12. Hallgren T. and Ranta A. "An Extensible Proof Text Editor". M. Parigot & A. Voronkov (eds), Logic for Programming and Automated Reason ing (LPAR'2000), LNCS/LNAI. 1955. P. 70 – 84, Springer Verlag, Heidelberg, 2000.
13. 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.
14. Coquand T. Domain Models in Type Theory. URL: (Slides: http://www.cs.chalmers.se/~coquand/type.html).
15. Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на С++. — Изд-во Бином, 1998. — 560 с.
16. 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.
17. Gordon M., Milner R. and Wadsworth C. Edinburgh LCF: A Mechanized Logic of Computation. Lect. Notes in Comp. Sci, V. 78. 1979.
18. Paulson L. Interactive Theorem Proving with Cambridge LCF. Tech. rep. 80, Computer Laboratory, Univ. of Cambridge, Nov. 1985.
19. Petersson K. A programming system for type theory. Tech. Rep.21, Programming Methodology Group, Univ. of Gotheborg / Chalmers Institute of Technology. Mar. 1982.
20. Coquand T., Huet G. Constructions: A higher-order proof system for machanized mathematics. In: EUROCAl'85: European Conference on Com- puter Algebra (1985), B. Buchberger, Ed., Vol. 203 of Lecture Notes in Com- puter Science, Spinger. P.151 – 184.
21. Constable R. L. et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986.
22. Luo Z. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Oxford, 1994.
23. Luo Z. PAL+: A lambda-free logical framework. J. Functional Programming, 2001.
24. Luo Z., Pollack R. Lego Proof Developmnet System: user's manual, LFCS Report ECS–LFCS–92–211, department of computer science, University of Edinburgh.
25. Callaghan P. and Luo Z. Plastic: an implementation of typed LF with coercive subtyping and universes. Submitted to Proc. LFM'99, 2000.
26. Soloviev S., Luo Z. Coercion Completion and Conservativity in Coercive Subtyping. Annals of Pure and Applied Logic. 113 (2002). 297 – 322.
27. McBride C. Faking It: Simulating Dependent Types in Haskell. J.
28. 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.
29. Coquand T. and Huet G. The calculus of constructions. Information and Computation , 76(2/3):95–120. February/March 1988.
30. 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.
31. Матулис В. А. Первый всесоюзный симпозиум по проблеме машинного поиска логического вывода. — Успехи мат. наук. — T. XIX, вып. 6. — 1964. — С. 239 – 241.
32. Шанин Н. А., Давыдов Г. В., Маслов С. Ю., Минц Г.Е., Оревков В.П., Слисенко А. О. Алгорифм машинного поиска естественного логиче- ского вывода в исчислении высказываний. — «Наука», 1965. — 39 с. [in: Automation of reasoning, Springer-Verlag, Berlin. Vol.1. P. 424 – 483, 1983].
33. Маслов С. Ю. Обратный метод установления выводимости в классическом исчислении предикатов. — Докл. АН СССР. — Т.159, №.1. — 1964. — С. 17 – 20.
34. Давыдов Г. В., Маслов С. Ю., Минц Г.Е., Оревков В.П., Слисенко А. О. Машинный алгорифм установления выводимости на основе о об- ратного метода. — Зап. научн. семинаров ЛОМИ. — 1969. — Т .16. — С. 8 – 19.
35. Niqui M. Constructive Reals in Coq: Axioms and First Order Equiva-
lence, Types 2000 Workshop, December 7–12 2000. Univ. of Durham.
36. 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.
37. Carpetta V. Certifying Fast Fourier Transform with Coq. Manuscript.
38. Frank Pfenning and Carsten Schermann. System description: Twelf - a meta-logical framework for deductive systems. In H. Ganzinger, editor, Pro- ceedings of the 16th International Conference on Automated Deduction (CADE-16), Trento, Italy, July 1999. Springer-Verlag LNAI 1632. P. 202 –
206.
39. Соловьев С.В. Категория конечных множеств и декартово замкну- тые категории. — Зап. Научных семинаров ЛОМИ. — 1981. — Т. 105. — С. 174 – 194.
40. Di Cosmo R. Isomorphism of Types. Burkhauser, 1995.
41. Chemouil D., Soloviev S. Extensional Isomorphisms of Inductive Types in Simply Typed Lambda-calculus. — 15 p. Submitted.
42. Федорченко Л. Н., Соловьев С. В. Cинтаксические преобразования
в системе SynGT и их новые приложения // Материалы VIII Санкт- Петербургской международной конференции «Региональная информати- ка–2002». — Ч. 2. — СПб: СПОИСУ, 2002. — С. 50.
43. Fedorchenko L. N., Soloviev S. V., Naumov I. N., Mehats L. Syntax Graph Transformations in the System SynGT and their Applications. — Rap- port IRIT/2003-06-R. UMR 5505 CNRS-INP-UPS. 15 pp. (English).
44. Fedorchenko L. and Baranov S. Equivalent Transformations and Regu-
larization in Context–Free Grammars. Bulgarian Academy of Sciences. Cyber- netics and Information Technologies (CIT). Vol. 14. No. 4. P. 11–28. Sofia 2015 (Scopus).
45. Федорченко Л. Н. SynGT: применение атрибутов // Региональная информатика и информационная безопасность. — Сб. трудов. — Вып. 1. — СПб.: СПОИСУ, 2015. — С. 68 – 73.
46. Boisvert B., Feraud L., Soloviev S. Typed lambda terms in categorical graph rewriting // In The International Conference Polynomial Computer Alge- bra, April 18-22, 2011. Saint-Petersburg, Russia, Euler International Mathe- matical Institute.VVM Publishing. P. 9 – 16.
47. Баранов С. Н., Буавер Б., Соловьев С. В., Феро Л. Некоторые при-
ложения лямбда-исчислений с типами к атрибутным вычислениям в сис-
темах категорных преобразований графов // Труды СПИИРАН. —
2012. — Вып. 23. — С. 296 – 323.
Статья.pdf