中国科学院机构知识库网格
Chinese Academy of Sciences Institutional Repositories Grid
首页 机构 成果 学者
  
  1. CAS IR Grid
  2. 计算技术研究所
  3. 中国科学院计算技术研究所
  4. 中国科学院计算技术研究所期刊论文
  5. 英文
The M-computations induced by accessibility relations in nonstandard models M of Hoare logic

文献类型：期刊论文

作者Cao, Cungen1; Sui, Yuefei1; Zhang, Zaiyue2
刊名FRONTIERS OF COMPUTER SCIENCE
出版日期2016-08-01
卷号10期号:4页码:717-725
关键词Hoare logic recursive function computable function nonstandard model of Peano arithmetic
ISSN号2095-2228
DOI10.1007/s11704-015-4024-2
英文摘要Hoare logic [1] is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure [2]. In a model M of Hoare logic, each program alpha induces an M-computable function f (alpha) (M) on the universe of M; and the M-recursive functions are defined on M. It will be proved that the class of all the M-computable functions f (alpha) (M) induced by programs is equal to the class of all the M-recursive functions. Moreover, each M-recursive function is -definable in M, where the universal quantifier is a number quantifier ranging over the standard part of a nonstandard model M.
资助项目National Natural Science Foundation of China[91224006] ; National Natural Science Foundation of China[61035004] ; National Natural Science Foundation of China[61173063] ; National Natural Science Foundation of China[61203284]
WOS研究方向Computer Science
语种英语
WOS记录号WOS:000379533100011
出版者HIGHER EDUCATION PRESS
源URL[http://119.78.100.204/handle/2XEOYT63/8276]  
专题中国科学院计算技术研究所期刊论文_英文
通讯作者Cao, Cungen
作者单位1.Chinese Acad Sci, Inst Comp Technol, Key Lab Intelligent Informat Proc, Beijing 100190, Peoples R China
2.Jiangsu Univ Sci & Technol, Dept Comp Sci, Zhenjiang 212003, Peoples R China
推荐引用方式
GB/T 7714		 Cao, Cungen,Sui, Yuefei,Zhang, Zaiyue. The M-computations induced by accessibility relations in nonstandard models M of Hoare logic[J]. FRONTIERS OF COMPUTER SCIENCE,2016,10(4):717-725.
APA Cao, Cungen,Sui, Yuefei,&Zhang, Zaiyue.(2016).The M-computations induced by accessibility relations in nonstandard models M of Hoare logic.FRONTIERS OF COMPUTER SCIENCE,10(4),717-725.
MLA Cao, Cungen,et al."The M-computations induced by accessibility relations in nonstandard models M of Hoare logic".FRONTIERS OF COMPUTER SCIENCE 10.4(2016):717-725.

入库方式： OAI收割

来源：计算技术研究所

浏览0
下载0
收藏0
其他版本

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。