Testing and proving distributed algorithms in constructive type theory

被引：0

作者：

Haiyan, Qiao ^{[1
]}

机构：

[1] Sun Yat Sen Univ, Dept Comp Sci, Guangzhou 510275, Peoples R China

来源：

TESTS AND PROOFS | 2007年 / 4454卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We report our experiences to verify distributed algorithms in constructive type theory by testing and proving. Properties can be tested to eliminate bugs before proving, thus saving expensive proof effort. Both deadlock property and liveness property are proven after testing. The verified algorithm can be executed in Cayenne, a functional programming language with dependent types.

引用

页码：79 / 94

页数：16

共 50 条

[21] Affine bracket algebra theory and algorithms and their applications in mechanical theorem proving
Ning Zhang
Hong-bo Li
Science in China Series A: Mathematics, 2007, 50 : 941 - 950
[22] Bar Induction is Compatible with Constructive Type Theory
Rahli, Vincent
Bickford, Mark
Cohen, Liron
Constable, Robert L.
JOURNAL OF THE ACM, 2019, 66 (02)
[23] Reading between the lines in constructive type theory
Turner, R
JOURNAL OF LOGIC AND COMPUTATION, 1997, 7 (02) : 229 - 250
[24] PROGRAM-DEVELOPMENT IN CONSTRUCTIVE TYPE THEORY
GALMICHE, D
THEORETICAL COMPUTER SCIENCE, 1992, 94 (02) : 237 - 259
[25] INTERNALISING MODIFIED REALISABILITY IN CONSTRUCTIVE TYPE THEORY
Palmgren, Erik
LOGICAL METHODS IN COMPUTER SCIENCE, 2005, 1 (02)
[26] Affine bracket algebra theory and algorithms and their applications in mechanical theorem proving
Ning ZHANG~(1+) Hong-bo LI~2 1 China Institute for Actuarial Science (CIAS)
2 Academy of Mathematics and Systems Science
Science in China(Series A:Mathematics), 2007, (07) : 941 - 950
[27] A Constructive Approach for Proving Data Structures' Linearizability
Lev-Ari, Kfir
Chockler, Gregory
Keidar, Idit
DISTRIBUTED COMPUTING (DISC 2015), 2015, 9363 : 356 - 370
[28] Towards a formalisation of relational database theory in constructive type theory
Gonzalía, C
RELATIONAL AND KLEENE-ALGEBRAIC METHODS IN COMPUTER SCIENCE, 2003, 3051 : 137 - 148
[29] Learning theory of distributed spectral algorithms
Guo, Zheng-Chu
Lin, Shao-Bo
Zhou, Ding-Xuan
INVERSE PROBLEMS, 2017, 33 (07)
[30] Affine bracket algebra theory and algorithms and their applications in mechanical theorem proving
Zhang, Ning
Li, Hong-bo
SCIENCE IN CHINA SERIES A-MATHEMATICS, 2007, 50 (07): : 941 - 950

← 1 2 3 4 5 →