定理证明器Coq与机械语义研究

THEOREM PROVER COQ AND RESEARCH OF MECHANISED SEMANTICS

随着证明理论和定理证明器的不断发展与成熟,形式语义研究已经从传统的基于手工证明的研究进入到机器可处理的机械语义的研究。交互式定理证明器Coq具备强大的描述能力,可以形式化地描述程序语法和语义,利用其内置函数式编程语言实现对程序语义的复杂操作,通过其证明系统形式地证明操作的正确性。根据形式语义的理论,针对简单类型Lambda演算的操作语义和指称语义,展示了如何利用定理证明器Coq的归纳定义实现它们的形式描述,并对语义的重要属性进行证明,表明机械语义是确保基础软件正确性的基础。

With the continuous development and maturity of proof theory and theorem provers,the research on formal semantics has been entered into studying mechanised semantics processable by machines from conventional study based on paper-and-pencil proving manner. Interactive theorem prover Coq possesses powerful description ability and can formally describe the syntax and semantics of program.We use its built-in functional programming language to achieve complex operation on program semantics,and formally prove the correctness of operation through its proof system.According to the theory of formal semantics,we demonstrate how to use inductive definitions of theorem prover Coq to realise their formal description aiming at the operational and denotational semantics of simple-type Lambda calculus,and prove the important property of semantics,which demonstrates that mechanised semantics is the basis for ensuring the correctness of basic software.