• Articles • Previous Articles     Next Articles

Constructive Sets in Computable Sets

Mi Thxi;   

  1. Department of Computer Science; Shanghai Jiaotong University; Shanghai 200030;
  • Online:1997-09-10 Published:1997-09-10

The original interpretation of the constructive set theory CZF in Martin-Lof's type theory uses the 'extensional identity types'. It is generally believed that these 'types' do not belong to type theory. In this paper it will be shown that the interpretation goes through without identity types. This paper will also show that the interpretation can be given in an intensional type theory. This reflects the computational nature of the interpretation. This computational aspect is reinforced by an w-Set model of…

Key words: ad hoc wireless network; multicast routing; protocol; dynamic ring;

[1] Aczel P. The type theoretic interpretation of constructive set theory. In Logic Colloquium '77, Macintyre A, Pacholski L, Paris J eds., North-Holland, 1978, pp.55-66.

[2] Troelstra A, van Dalen D. Constructivism in Mathematics: An Introduction, II. North-Holland, 1988.

[3] Nordstrom B, Petersson K, Smith J. Programming in Martin-Lof's type theory-An introduction. In International Series of Monographs on Computer Science 7, Oxford University Press, 1990. ……….
[1] Ibrahim S. Alsukayti. Quality of Service Support in RPL Networks: Standing State and Future Prospects [J]. Journal of Computer Science and Technology, 2022, 37(2): 344-368.
[2] Ding-Huang Hu, De-Zun Dong, Yang Bai, Shan Huang, Ze-Jia Zhou, Zi-Hao Wei, Xiang-Ke Liao. Harmonia: Explicit Congestion Notification and Credit-Reservation Transport Converged Congestion Control in Datacenters [J]. Journal of Computer Science and Technology, 2021, 36(5): 1071-1086.
[3] Jia-Qi Yin, Hui-Biao Zhu, Yuan Fei. Specification and Verification of the Zab Protocol with TLA+ [J]. Journal of Computer Science and Technology, 2020, 35(6): 1312-1323.
[4] Heng-Feng Wei, Rui-Ze Tang, Yu Huang, Jian Lv. Jupiter Made Abstract, and Then Refined [J]. Journal of Computer Science and Technology, 2020, 35(6): 1343-1364.
[5] Xiao-Jun Zhu, Li-Jie Xu, Xiao-Bing Wu, Bing Chen. Minimum Time Extrema Estimation for Large-Scale Radio-Frequency Identification Systems [J]. Journal of Computer Science and Technology, 2020, 35(5): 1099-1114.
[6] Chi Zhang, Jun-Rong Liu, Da-Wu Gu, Wei-Jia Wang, Xiang-Jun Lu, Zheng Guo, Hai-Ning Lu. Side-Channel Analysis for the Authentication Protocols of CDMA Cellular Networks [J]. Journal of Computer Science and Technology, 2019, 34(5): 1079-1095.
[7] Shou-Wan Gao, Peng-Peng Chen, Xu Yang, Qiang Niu. Multi-Sensor Estimation for Unreliable Wireless Networks with Contention-Based Protocols [J]. Journal of Computer Science and Technology, 2018, 33(5): 1072-1085.
[8] Yang Li, Zhi-Ping Cai, Hong Xu. LLMP: Exploiting LLDP for Latency Measurement in Software-Defined Data Center Networks [J]. , 2018, 33(2): 277-285.
[9] Li-Jing Wang, Yong-Qiang Lv, Ilya Moiseenko, Dong-Sheng Wang. A Dataflow-Oriented Programming Interface for Named Data Networking [J]. , 2018, 33(1): 158-168.
[10] Mert Ozkaya. Visual Specification and Analysis of Contract-Based Software Architectures [J]. , 2017, 32(5): 1025-1043.
[11] Mao-Lin Yang, Hang Lei, Yong Liao, Furkan Rabee. Improved Blocking Time Analysis and Evaluation for the Multiprocessor Priority Ceiling Protocol [J]. , 2014, 29(6): 1003-1013.
[12] Aditya Wagh, Yunfei Hou, Chunming Qiao, Longfei Zhang, Xu Li, Adel Sadek, Kevin Hulme, Changxu Wu, Hong-Li Xu, and Liu-Sheng Huang. Emerging Applications for Cyber Transportation Systems [J]. , 2014, 29(4): 562-575.
[13] Cheng Bo, Junze Han, Xiangyang Li, Yu Wang, and Bo Xiao. SA-MAC:Self-stabilizing Adaptive MAC protocol for Wireless Sensor Networks [J]. , 2014, 29(4): 605-617.
[14] Jing-Jie Liu, Lei Nie. A Functional Sensing Model and a Case Study in Household Electricity Usage Sensing [J]. , 2014, 29(2): 182-193.
[15] Bing-Qing Shao, Jun-Wei Zhang, Cai-Ping Zheng, Hao Zhang, Zhen-Jun Liu, Lu Xu . A Non-Forced-Write Atomic Commit Protocol for Cluster File Systems [J]. , 2014, 29(2): 303-315.
Full text



[1] Jin Lan; Yang Yuanyuan;. A Modified Version of Chordal Ring[J]. , 1986, 1(3): 15 -32 .
[2] Fan Zhihua;. Vectorization for Loops with Three-Forked Jumps[J]. , 1988, 3(3): 186 -202 .
[3] Xue Xing; Sun Zhongxiu; Zhou Jianqiang; Xu Xihao;. A Message-Based Distributed Kernel for a Full Heterogeneous Environment[J]. , 1990, 5(1): 47 -56 .
[4] Guo Qingping; Y. Paker;. Communication Analysis and Granularity Assessment for a Transputer-Based System[J]. , 1990, 5(4): 347 -362 .
[5] Liao Xianzhi; Jin Lan;. A Mechanism Supporting the Client/Server Relationship in the Operating System of Distributed System “THUDS”[J]. , 1991, 6(3): 256 -262 .
[6] Sun Yufang;. The UNIX Localization and Chinese Information Processing System[J]. , 1991, 6(4): 370 -375 .
[7] Xu Manwu;. An Implementation of Pure Horn Clause Logic Programming in a Reduction System[J]. , 1993, 8(3): 53 -61 .
[8] Zhou Yong; Tang Zesheng;. Constructing Isosurfaces from 3D Data Sets Taking Account of Depth Sorting of Polyhedra[J]. , 1994, 9(2): 117 -127 .
[9] Liao Lejian; Shi Zhongzhi;. Minimal Model Semantics for Sorted Constraint Representation[J]. , 1995, 10(5): 439 -446 .
[10] Zhao Yu; Zhang Qiong; Xiang Hui; Shi Jiaosing; He Zhijun;. A Simplified Model for Generating 3D Realistic Sound in the Multimedia and Virtual Reality Systems[J]. , 1996, 11(4): 461 -470 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved