期刊文献+

构造类型论与计算机程序设计 被引量:1

Type System and Computer Programming
下载PDF
导出
摘要 1.引言近些年来,在计算机程序设计语言理论、自动演绎以及更一般的逻辑和计算领域研究中,出现了多种以构造类型论为基础的系统,如LCF、ALF、LEGO、Coq等,它们被用来为程序设计语言设计类型系统,进行程序开发和验证、形式化证明以及作为数学和计算的基础.构造类型论为计算机科学家提供了一个框架,以一种优雅和灵活的方式把逻辑和程序设计语言结合起来:在同一形式系统中,可以同时表达规约和(函数式语言)程序,从证明规则可以导出正确的程序,并验证程序具有某种性质,从而在同一系统内完成程序的开发和验证[26,19]. Recent years, in the area of computer programming language theories, automated deduction, and more generalized area of logic and computing, a lot of systems based on constructive type theory are used widely to design type system for computer programming languages, to do formal system development and verification, and to be used as foundation of mathematics and computing. Constructive type theory provides computer scientists with a framework to combine logic and computer program design in an elegant and flexible way. In this paper, the evolvement of constructive type theory is first introduced. The several foundations of type theory are then discussed, together with analysis of the relationships between them. The relation between constructive type theory and computer programming is explored in-depth. In the last, Martin Lof's intuitionistic type theory is used as an example to demonstrate how to do program development and verification in the same formal system.
出处 《计算机科学》 CSCD 北大核心 2002年第2期72-77,61,共7页 Computer Science
基金 国家自然科学基金69931040 国防科研基金GF00J6.2.1.JB0501
关键词 限制谓词演算 构造类型论 构造数学 计算机 程序设计 程序设计语言 Constructive type theory,Type theory, Intuitionistic logic, Automated deduction, Lambda calculus, Proof theory
  • 相关文献

参考文献41

  • 1Barendregt H. The Lambda Calculus its Syntax and Semantics.North-Holland, 1981 被引量:1
  • 2Barendregt H P. Lambda calculi with types. In: Samson Abramsky, Dov. M. Gabbay,Thomas S. E. Maibaum, eds, Handbook of Logic in Computer Science. Oxford University Press, 1992,2:117~309 被引量:1
  • 3Curry H B,Reys R. Combinatory Logic, vol. I. North-Holland,1958 被引量:1
  • 4Hankin C L, Lambda Calculi. A Guide for Computer Scientists.Graduate Texts in Computer Science, Oxford University Press,1994,3 被引量:1
  • 5Hindley J R,Seldin J P. Introduction to combinators and λ-calculus. Cambridge University Press, 1986 被引量:1
  • 6Gunter C A. Semantics of programming languages: structures and techniques. Foundations of computing. In:M. Garey,and A. Meyer eds. MIT Press, 1992 被引量:1
  • 7Cardelli L, Wegner P. On Understanding Types, Data Abstraction, and Polymorphism. ACM Computing Surveys, 1985,17 (4) :471~521 被引量:1
  • 8Milner R, Tofte M, Harper R. The Definition of Standard ML.The MIT Press, 1991 被引量:1
  • 9Hudak P,et al. Report on the Programming Language Haskell: A Non-Strict, Purely Functional Language, March 1992. Version 1.2. Also in Sigplan Notices, May 1992 被引量:1
  • 10Mitchell J C. Type Systems for programming languages. In Handbook of Theoretical Computer Science, J. Van Leeuwen, ed.North Holland. 1990. 365~458 被引量:1

同被引文献10

  • 1庞建民,赵荣彩,王怀民.Haskell语言的高阶特性及其应用[J].计算机科学,2005,32(6):167-168. 被引量:8
  • 2Berger U,Berghofer S.Program extraction from normalization proofs,2005 被引量:1
  • 3Nordstrom B,Petersson K,Smith J.Programming in Martin-Lof's type theory.An introduction.Oxford University Press,1990 被引量:1
  • 4The Coq Developmem Team.The Coq Proof Assistant Reference Manual(Version 8.O),2005 被引量:1
  • 5Barendregt H P.Lambda calculi with types.In:Samson Abramsky.Dov.M.Gabbay.Thomas S.E.M aibaum,eds.Handbook of Logic in Computer Science.Oxford University Press,1992,2 被引量:1
  • 6Coquand T,Huet G.The calculus of constructions.Information and Computation,1988 被引量:1
  • 7Letouzey P.Certified functional programming.Program extraction within Coq proof assistant:[PhD manuscript].2004.7 被引量:1
  • 8Heine M,Urzyczyn P.Lectures on the Curry-Howard Isomorphism.1998.5 被引量:1
  • 9Letouzey P.A New Extraction for Coq.Types for Proofs and Programs,Second InternationalWorkshop.Springer-Verlag,2003 被引量:1
  • 10郝宁湘.构造性数学及其哲学意义[J].自然辩证法通讯,1997,19(3):22-28. 被引量:7

引证文献1

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部