ROOSTERIZE: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning

摘要: Naming conventions are an important concern in large verification projects using proof assistants, such as Coq. In particular, lemma names used by engineers to effectively understand and modify Coq code. However, providing accurate informative is a complex task, which currently often carried out manually. Even when naming automated rule-based tools, generated may fail adhere not specified explicitly. We demonstrate toolchain, dubbed Roosterize, automatically suggests projects. Roosterize leverages neural network model trained on existing code, thus avoiding manual specification of conventions. To allow conveniently access suggestions from during project development, we integrated the toolchain into popular Visual Studio Code editor. Our evaluation shows that substantially outperforms strong baselines for suggesting useful practice. The demo video can be viewed at: this https URL.