Верификация преобразования грамматики в нормальную форму Хомского в F
https://doi.org/10.15514/ISPRAS-2016-28(2)-8
Аннотация
Об авторах
М. И. Полубелова
Санкт-Петербургский государственный университет
Россия
Россия
С. Н. Божко
Санкт-Петербургский государственный университет
Россия
Россия
С. В. Григорьев
Санкт-Петербургский государственный университет
Россия
Россия
Список литературы
1. H. Geuvers. Proof assistants: History, ideas and future. Sadhana, 2009, vol. 34, issue 1. pp. 3–25. DOI: 10.1007/s12046-009-0001-5.
2. A. Chlipala. Certified programming with dependent types. MIT Press, 2013, 440 p.
3. T. Sheard, A. Stump, S. Weirich. Language-based verification will change the world. Proceedings of the FSE/SDP workshop on Future of software engineering research, 2010, pp. 343–348. DOI: 10.1145/1882362.1882432.
4. E. Tanter, N. Tabareau. Gradual certified programming in Coq. Proceedings of the 11th Symposium on Dynamic Languages, 2015. pp. 26–40. DOI: 10.1145/2816707.2816710.
5. The Coq proof assistant. June 2016. https://coq.inria.fr/
6. U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, 2007.
7. The F* homepage. June 2016. https://www.fstar-lang.org/
8. E. Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 2013, vol. 23, n. 5, pp. 552–593. DOI: 10.1017/S095679681300018X.
9. N. Swamy, C. Hritcu, C. Keller. Dependent Types and Multi-monadic Effects in F*. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016, pp. 256–270. DOI: 10.1145/2837614.2837655
10. The YaccConstructor homepage. June 2016. https://github.com/YaccConstructor/
11. I. Kirilenko, S. Grigorev, D. Avdiukhin. Syntax analyzers development in automated reengineering of informational system. St. Petersburg State Polytechnical University Journal. Computer Science. Telecommunications and Control Systems, 2013, no. 174, pp. 94 – 98.
12. J.-H. Jourdan, F. Pottier, X. Leroy. Validating LR (1) parsers. Programming Languages and Systems, 2012, pp. 397–416.
13. K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. International Conference on Logic for Programming Artificial Intelligence and Reasoning, 2010, pp. 348–370.
14. J.-C. Filliatre, A. Paskevich. Why3: Where Programs Meet Provers. Proceedings of the 22Nd European Conference on Programming Languages and Systems, 2013, pp. 125–128. DOI: 10.1007/978-3-642-37036-6_8.
15. B. C. Pierce. Types and Programming Languages. MIT Press, 2002, 645 p.
16. F* tutorial. June 2016. https://www.fstar-lang.org/tutorial/
17. D. Syme, A. Granicz, A. Cisternino. Expert F#. Apress, 2012, 609 p.
18. D. Firsov, T. Uustalu. Certified normalization of context-free grammars. Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015, pp. 167–174. DOI: 10.1145/2676724.2693177.
19. Verification of grammar transformation to Chomsky normal form in F*. June 2016. https://github.com/YaccConstructor/YC_FStar.
Рецензия
Для цитирования:
Полубелова М.И., Божко С.Н., Григорьев С.В. Верификация преобразования грамматики в нормальную форму Хомского в F. Труды Института системного программирования РАН. 2016;28(2):127-138. https://doi.org/10.15514/ISPRAS-2016-28(2)-8
For citation:
Polubelova M.I., Bozhko S.N., Grigorev S.V. Certified Grammar Transformation to Chomsky Normal Form in F. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(2):127-138. https://doi.org/10.15514/ISPRAS-2016-28(2)-8
Послать статью по эл. почте 