基于Coq的命令式语言编译器机械验证的研究与实现
盛枫,窦亮,杨宗源
Research and Implementation of the Mechanization Verification of a Coqbased Imperative Language Compiler
SHENG Feng,DOU Liang,YANG Zong-yuan
小型微型计算机系统 . 2015, (9): 1927 -1931 .