CAJ | 학술논문

随着证明理论和定理证明器的不断发展与成熟，形式语义研究已经从传统的基于手工证明的研究进入到机器可处理的机械语义的研究。交互式定理证明器 Coq 具备强大的描述能力，可以形式化地描述程序语法和语义，利用其内置函数式编程语言实现对程序语义的复杂操作，通过其证明系统形式地证明操作的正确性。根据形式语义的理论，针对简单类型 Lambda 演算的操作语义和指称语义，展示了如何利用定理证明器 Coq 的归纳定义实现它们的形式描述，并对语义的重要属性进行证明，表明机械语义是确保基础软件正确性的基础。
수착증명이론화정리증명기적불단발전여성숙，형식어의연구이경종전통적기우수공증명적연구진입도궤기가처리적궤계어의적연구。교호식정리증명기 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.