%0 Journal Article
%T A Survey of Curry-Howard Isomorphism<br>Curry—Howard同构理论：研究综述
%A 张昱
%A 宋方敏
%J 计算机科学
%D 2002
%I 
%X 一、引言理论计算机科学的发展吸取了大量数学和逻辑上的重要成果。逻辑是理论计算机科学十分重要的基础之一,而其中又以直觉主义逻辑对计算机科学的影响最为显著,它的思想比古典逻辑更加切合计算的观点。另一个值得一提的成果就是Alonzo Church在1936年提出的λ-演算系统,λ-演算所依据的是一种完全不同于逻辑的思想,它是计算机科学中函数式程序设计语言的理论基础。这是两种无论从语祛上还是从语义上去观察都区别甚大的形式系统,然而它们之间却存在着某种奇妙的对应关系,这就是本文所要介绍的Curry-Howard同构理论(Curry-Howard Isomorphism)。
%K 计算机科学
%K Curry－Howard同构理论
%K 直觉主义逻辑
%K 命题演算
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=AC509E5EB3467567&yid=C3ACC247184A22C1&vid=771469D9D58C34FF&iid=E158A972A605785F&sid=9CF7A0430CBB2DFD&eid=708DD6B15D2464E8&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=11