Lectures on the Curry-Howard Isomorphism, Volume 149 豆 0.0分

资源最后更新于 2020-08-23 08:23:34

作者：Morten Heine Sørensen M.Sc Ph.D

出版社：Elsevier Science

出版日期：2006-01

ISBN：9780444520777

文件格式： pdf

标签： 类型论 理论计算机 计算机科学 程序设计语言 数理逻辑 命题逻辑 theory proof

简介· · · · · ·

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calcul...