Innovations in computational type theory using Nuprl
Journal of Applied Logic(2006)
摘要
For twenty years the Nuprl (“new pearl”) system has been used to develop software systems and formal theories of computational mathematics. It has also been used to explore and implement computational type theory (CTT)—a formal theory of computation closely related to Martin-Löf's intuitionistic type theory (ITT) and to the calculus of inductive constructions (CIC) implemented in the Coq prover.
更多查看译文
关键词
Martin-Löf type theory,Dependent intersection types,Union types,Polymorphic subtyping,Logic of events,Formal digital libraries,Computational type theory,Proofs as programs,Program extraction,Tactics
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要