Certified Grammar Transformation to Chomsky Normal Form in F

Certified programming allows to prove that the program meets its specification. The check of correctness of a program is performed at compile time, which guarantees that the program always runs as specified. Hence, there is no need to test certified programs to ensure they work correctly. There are numerous toolchains designed for certified programming, but F* is the only language that support both general-purpose programming and semi-automated proving. The latter means that F* infers proofs when it is possible and a user can specify more complex proofs if necessary. We work on the application of this technique to a grammarware research and development project YaccConstructor. We present a work in progress verified implementation of transformation of Context-free grammar to Chomsky normal form, that is making progress toward the certification of the entire project. Among other features, F* system allows to extract code in F# or OCaml languages from a program written in F*. YaccConstructor project is mostly written in F#, so this feature of F* is of particular importance because it allows to maintain compatibility between certified modules and those existing in the project which are not certified yet. We also discuss advantages and disadvantages of such approach and formulate topics for further research.

certified programming, F*, program verification, context-free grammar, Chomsky normal form, grammar transformation, dependent type, refinement type

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.