%0 Journal Article
%T Verification of Semantic Properties Based on Logical Framework<br>基于逻辑框架LF的语义性质之验证
%A PANG Jian-Min
%A ZHAO Rong-Cai
%A WANG Huai-Min
%A <br>庞建民
%A 赵荣彩
%A 王怀民
%J 计算机科学
%D 2006
%I 
%X 本文对基于类型理论逻辑框架（LF）的语义性质验证加以研究，针对函数式语言LAZY-PCF＋SHAR，利用计算机辅助推理方法和技术给出相应的形式化描述及相关性质证明，从而提倡严格的和计算机辅助的证明在语义性质验证方面的应用。同时，考察了LF以及其实现系统Plastic的能力。
%K Type theory
%K Logic framework
%K Verification of semantic properties
%K Operational semantics
%K Functional programming<br>类型理论
%K 逻辑框架
%K 语义性质验证
%K 操作语义
%K 函数式语言
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=0B31EDC558244CB2&yid=37904DC365DD7266&vid=27746BCEEE58E9DC&iid=94C357A881DFC066&sid=59906B3B2830C2C5&eid=7801E6FC5AE9020C&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=22