Λ演算

作品数：10被引量：21H指数：2
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：江南何炎祥李清安宋国新丁志义更多>>
相关机构：南京大学上海交通大学武汉大学湖北工业大学更多>>
相关期刊：《福州大学学报（自然科学版）》《小型微型计算机系统》《程序员》《语数外学习（高中版）（下）》更多>>
相关基金：国家自然科学基金博士科研启动基金国家教育部博士点基金国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
机械化定理证明研究综述被引量：13
《软件学报》2020年第1期82-112,共31页江南 李清安 汪吕蒙 张晓瞳 何炎祥 
国家自然科学基金(90818018,91018009,61170022,91118003,61373039);华为技术有限公司合作项目(YB2015090035);湖北工业大学校博士科研启动基金(BSQD2017043)。
随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明...
关键词：定理证明 证明助手 消解 自然演绎 类型化的λ演算 编程逻辑 求精 
计算的极限(三):函数构成的世界
《语数外学习（高中版）（下）》2018年第9期62-65,共4页
计算无处不在.走进一个机房,在服务器排成的一道道墙之间,听着风扇的鼓噪,似乎能嗅出0和1在CPU和内存之间不间断的流动.从算筹算盘,到今天的计算机,我们用作计算的工具终于开始量到质的飞跃.计算机能做的事情越来越多,甚至超越了它们的...
关键词：Λ演算 数学概念 
焦点视角下黄犬奔马句的语义分析
《湘南学院学报》2012年第6期65-68,共4页谭晖 朱秀梅 
黄犬奔马句是修辞学工拙论的经典句,对黄犬奔马句的语义进行分析,可以从各句中论元的论旨角色的区分,了解句子的信息分布结构,还可以通过焦点与预设、焦点的三分结构和λ演算得出黄犬奔马句多种语义解释。这些语义分析体现了焦点对汉语...
关键词：黄犬奔马句 焦点 三分结构 Λ演算 语义解释 
函数式编程思想被引量：2
《程序员》2010年第9期24-24,共1页俞黎敏 
函数式编程是种编程范型，将计算机运算视为函数的计算。函数编程语言最重要的基础是λ演算（Lambda Calculus）。而且λ演算的函数可以接受函数当作输入（引数）和输出（传出值）。与命令式编程相比，函数式编程强调函数的计算比指令...
关键词：编程思想 函数式 计算机运算 编程范型 编程语言 Λ演算 输入 命令 
类型系统与程序正确性问题被引量：3
《计算机科学》2006年第1期141-143,157,共4页丁志义 宋国新 邵志清 
本文工作得到国家自然科学基金和中科院计算机科学重点实验室资助(编号:60373075;SYSKF0305)。
类型系统能检出合法程序的语义错误，可以缩短调试时间，在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子类型的高阶类型系统腿已成为类型化语言的演算核心。类型系统和直觉主义极小逻辑是同构的。证明系统...
关键词：类型系统 程序验证 Λ演算 证明理论 程序正确性 语义错误 执行程序 直觉主义 子类型 代码 
递归函数的π可定义性及其实现研究被引量：1
《小型微型计算机系统》2005年第10期1749-1753,共5页颜锋 陈韬略 韩婷婷 吕建 
国家重点基础研究发展规划"九七三"项目(2002CB312002)资助国家自然科学基金(60273034)资助国家"八六三"项目(2002AA116010)资助江苏省自然科学基金(BK2002203;BK2002409)资助.
并发计算模型是计算机科学研究的重要问题之一．π演算作为一个并发计算模型,是一种重要的移动进程演算,其中 的进程通过发送通信链接互相交互．与传统的进程代数如CCS相比,π演算有着更为良好的代数性质和表达能力．正如λ演算 能够描...
关键词：Π演算 Λ演算 π可定义性 递归函数 
类型系统的研究与进展被引量：2
《计算机科学》2000年第5期5-13,共9页周晓聪 李文军 李师贤 
高等学校博士学科点专项科研基金;资助号:99-018-411703
1 引言类型系统源于罗素为避免朴素集合论中的悖论而引入的“分类”思想。后来邱奇在他的λ演算中也引入了“类型”。60年代初出现的Algol语言提出了数据类型的概念。逻辑学家J.Girard和计算机科学家J.Reynold在70年代初为类型系统引入...
关键词：类型系统 Λ演算 面向对象 软件开发 
λ演算中的第二不动点定理
《软件学报》1996年第A00期381-384,共4页宋方敏 
作者研究λ演算中第二不动点的性质，首先关于第二不动点的３个例题之间的关系且证明了这们，然后为第二不动点组合子给以一个充分条件且作一系列的第二不动点组子，作者还提出和证明了多元第二不点宣。
关键词：Λ演算 第二不动点定理 命题演算 
抽象算法C-T-ABS和ABSTRACT的理论推导与等价性证明
《计算机研究与发展》1993年第12期1-11,共11页杨祥金 
国家自然科学基金DDFP
ABSTRACT,C-T-ABS 是把λ表达式转换成SKI 表达式的抽象算法,是函数式语言实现的理论基础。本文从λ演算、SKI 演算的基本理论出发,对这两个算法进行了理论推导及功能上的等价性证明。展示了对同一输入,C-T-ABS 能生成较优化的代码,并...
关键词：抽象算法 Λ演算 SKI演算 
带类型λ-演算的扩充
《福州大学学报（自然科学版）》1993年第3期8-15,共8页王美清 
在许多情况下λ－演算的能力不够、Felleisen M等把λ－演算加以扩充，并证明扩充后的语言λｃ具有某些基本性质．本文试图为λｃ－演算加上类型，给出带类型λｃ－演算的逻辑系统，然后考虑它的指称语义．
关键词：类型 Λ演算 λc演算 程序语言 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部