Interactive Theorem Proving for System Verification and Program Extraction

点击翻译按钮获取中文摘要

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).