BSU Bulletin. Mathematics, Informatics
Bibliographic description:
Type Theory, Computer Algebra, Proof Assistants and Grammars // BSU Bulletin. Mathematics, Informatics. - 2016. №2. . - С. 55-76.
Title:
Type Theory, Computer Algebra, Proof Assistants and Grammars
Financing:
Codes:
Annotation:
This article provides a brief overview and review of the main areas of research related to type theory and their applications. A description of universal systems of analytical calculations (Computer Algebra), as well as support systems of analytical calculations (Proof Assistants) are given. The application types in Computer Science, above all, functional and object-oriented programming has been discussed. Specialized the main research teams which are working out research and development of software systems in this area.
Keywords:
types, subtypes, formal systems, proof checking, graph transformations, grammars.
List of references:
1. Shanin N.A. Doklad na IV Vsesojuznom matematicheskom s#ezde v ijune 1961 g.
2. Whitehead, Alfred North, and Bertrand Russell (1910, 1912, 1913) Prin-cipia Mathematica, 3 vols, Cambridge: Cambridge University Press. Sec- ond edition, 1925 (Vol. 1), 1927 (Vols 2, 3). Abridged as Principia Mathe- matica 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 Differential 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 Expres-sions, 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. Buch G. Ob#ektno-orientirovannyj analiz i proektirovanie s pri-merami prilozhenij na S++. — Izd-vo Binom, 1998. — 560 s.
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 Mecha- nized 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 Coer- cive 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 Lan- guage 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, Gote- borg (Sweden), January 95.
31. Matulis V. A. Pervyj vsesojuznyj simpozium po probleme mashinnogo poiska logicheskogo vyvoda. — Uspehi mat. nauk. — T. XIX, vyp. 6. — 1964. — S. 239 – 241.
32. Shanin N. A., Davydov G. V., Maslov S. Ju., Minc G.E., Orevkov V.P., Slisenko A. O. Algorifm mashinnogo poiska estestvennogo logiche- skogo vyvoda v ischislenii vyskazyvanij. — «Nauka», 1965. — 39 s. [in: Automation of reasoning, Springer-Verlag, Berlin. Vol.1. P. 424 – 483, 1983].
33. Maslov S. Ju. Obratnyj metod ustanovlenija vyvodimosti v klas- sicheskom ischislenii predikatov. — Dokl. AN SSSR. — T.159, №.1. — 1964. — S. 17 – 20.
34. Davydov G. V., Maslov S. Ju., Minc G.E., Orevkov V.P., Slisenko A. O. Mashinnyj algorifm ustanovlenija vyvodimosti na osnove o ob-ratnogo me- toda. — Zap. nauchn. seminarov LOMI. — 1969. — T .16. — S. 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. Solov'ev S.V. Kategorija konechnyh mnozhestv i dekartovo zamknu- tye kategorii. — Zap. Nauchnyh seminarov LOMI. — 1981. — T. 105. — S. 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. Fedorchenko L. N., Solov'ev S. V. Cintaksicheskie preobrazovanija v sisteme SynGT i ih novye prilozhenija // Materialy VIII Sankt-Peterburgskoj mezhdunarodnoj konferencii «Regional'naja informati-ka–2002». — Ch. 2. — SPb: SPOISU, 2002. — S. 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. Cybernetics and Information Technologies (CIT). Vol. 14. No. 4. P. 11–28. Sofia 2015 (Scopus).
45. Fedorchenko L. N. SynGT: primenenie atributov // Regional'naja in- formatika i informacionnaja bezopasnost'. — Sb. trudov. — Vyp. 1. — SPb.: SPOISU, 2015. — S. 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.
2. Whitehead, Alfred North, and Bertrand Russell (1910, 1912, 1913) Prin-cipia Mathematica, 3 vols, Cambridge: Cambridge University Press. Sec- ond edition, 1925 (Vol. 1), 1927 (Vols 2, 3). Abridged as Principia Mathe- matica 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 Differential 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 Expres-sions, 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. Buch G. Ob#ektno-orientirovannyj analiz i proektirovanie s pri-merami prilozhenij na S++. — Izd-vo Binom, 1998. — 560 s.
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 Mecha- nized 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 Coer- cive 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 Lan- guage 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, Gote- borg (Sweden), January 95.
31. Matulis V. A. Pervyj vsesojuznyj simpozium po probleme mashinnogo poiska logicheskogo vyvoda. — Uspehi mat. nauk. — T. XIX, vyp. 6. — 1964. — S. 239 – 241.
32. Shanin N. A., Davydov G. V., Maslov S. Ju., Minc G.E., Orevkov V.P., Slisenko A. O. Algorifm mashinnogo poiska estestvennogo logiche- skogo vyvoda v ischislenii vyskazyvanij. — «Nauka», 1965. — 39 s. [in: Automation of reasoning, Springer-Verlag, Berlin. Vol.1. P. 424 – 483, 1983].
33. Maslov S. Ju. Obratnyj metod ustanovlenija vyvodimosti v klas- sicheskom ischislenii predikatov. — Dokl. AN SSSR. — T.159, №.1. — 1964. — S. 17 – 20.
34. Davydov G. V., Maslov S. Ju., Minc G.E., Orevkov V.P., Slisenko A. O. Mashinnyj algorifm ustanovlenija vyvodimosti na osnove o ob-ratnogo me- toda. — Zap. nauchn. seminarov LOMI. — 1969. — T .16. — S. 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. Solov'ev S.V. Kategorija konechnyh mnozhestv i dekartovo zamknu- tye kategorii. — Zap. Nauchnyh seminarov LOMI. — 1981. — T. 105. — S. 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. Fedorchenko L. N., Solov'ev S. V. Cintaksicheskie preobrazovanija v sisteme SynGT i ih novye prilozhenija // Materialy VIII Sankt-Peterburgskoj mezhdunarodnoj konferencii «Regional'naja informati-ka–2002». — Ch. 2. — SPb: SPOISU, 2002. — S. 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. Cybernetics and Information Technologies (CIT). Vol. 14. No. 4. P. 11–28. Sofia 2015 (Scopus).
45. Fedorchenko L. N. SynGT: primenenie atributov // Regional'naja in- formatika i informacionnaja bezopasnost'. — Sb. trudov. — Vyp. 1. — SPb.: SPOISU, 2015. — S. 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.
Article.pdf