Interactive Theorem Proving for System Verification and Program Extraction

主要目标：1；研究可证明正确的计算机程序自动合成逻辑的理论基础。为了开发一个原型，实现了沿着第一个目标的路线的程序提取。学生将证明显示提取程序正确性的一般定理，并将使用先进的编程技术（一元效应）来实现程序提取。该项目主要涉及理论计算机科学、逻辑学和组合学、验证和正确性等领域，但它也与数学分析（因为主要应用在分析中）、自然语言处理（因为系统将包含自然语言接口）、编程语言和编译器（因为需要开发提取语言的操作和指示语义）、人工智能技术（因为系统将有一个自动定理证明组件）。

Key Objectives: 1. To investigate the theoretical foundation of a logic for the automatic synthesis of provably correct computer programs.2. To develop a prototype the implements program extraction along the lines of the first objective.The student will prove general theorems showing the correctness of extracted programs and will use advanced programming techniques (monadic effects) to implement program extraction.The project mainly resides in the areas of Theoretical Computer Science, Logic and combinatorics, Verification and correctness, but it also intersects substantially with Mathematical analysis (since the main applications are in analysis), Natural language processing (since the system will contain a natural language interface), Programming languages and compilers (since the operational and denotational semantics of the extraction language needs to be developed), Artificial intelligence technologies (since the system will have an automatic theorem proving component).