第1章 数学基础 1
1.1 λ演算 1
1.2 格论 14
1.3 范畴论 32
1.4 不动点理论 56
1.5 Petri网论 64
1.6 Hilbert空间和相关拓扑、代数结构 82
1.7 概率和随机过程 95
1.8 矢列演算、线性逻辑、线性类型系统和线性带类型λ演算 107
1.8.1 从矢列演算讲起 107
1.8.2 线性逻辑 111
1.8.3 线性类型系统 118
第2章 操作语义 125
2.1 概述 125
2.2 SECD抽象机 133
2.3 维也纳定义语言 142
2.4 赫斯利方法和PL／ I标准 161
2.5 W文法及其抽象机 174
2.6 变换语义学 184
2.7 结构化的操作语义 199
第3章 指称语义 207
3.1 概述 207
3.2 指称语义的描述方法 225
3.3 函数式语言的指称语义 229
3.4 命令式语言：直接语义和继续语义 234
3.5 变量、说明和作用域 243
3.6 过程和函数 252
3.7 元语言META Ⅳ 264
3.8 域的递归理论 278
3.9 递归域的两个模型 287
3.10 幂域理论 303
3.11 不确定程序的指称语义 316
3.12 概率幂域和概率指称语义 322
3.13 基于概率不确定幂域的指称语义 332
3.14 计算理论的范畴论语义 344
第4章 公理语义 351
4.1 概述 351
4.2 Hoare公理系统 361
4.3 分程序的公理语义 373
4.4 过程的公理语义 382
4.5 联立子程序的公理语义 395
4.6 类程的公理语义 412
4.7 Pascal的公理语义 420
4.8 完备性和可表达性 431
4.9 过程公理的健康性和完备性 440
4.10 完全正确性 451
4.11 最弱前置条件和不确定性公理语义 461
4.12 最弱概率前置语义 472
4.12.1 概率程序的最弱前置语义 472
4.12.2 概率不确定程序的最弱前置语义 479
4.13 类型理论和程序逻辑 483
4.14 模态逻辑和时序逻辑 498
4.15 分支时序逻辑和线性时序逻辑 505
4.16 区间逻辑和时段演算 518
4.16.1 区间逻辑IL 518
4.16.2 时段演算DC 522
4.16.3 一个实例 527
4.17 动态逻辑 531
第5章 代数语义 539
5.1 概述 539
5.2 Σ代数和初始语义 545
5.3 扩充的公理形式 556
5.4 健康性、完备性和可判定性 565
5.5 充分完备性和层次一致性 577
5.6 理论描述语言Clear 583
5.7 代数语义的范畴论基础 591
5.8 终结语义 605
5.9 格语义 613
5.10 可观察性和观察等价性 620
5.11 偏Σ代数 635
5.12 模型描述语言ASL 648
5.13 程序设计语言的代数语义 657
5.14 带动态结构的程序的语义 667
第6章 并发和分布式程序的形式语义 679
6.1 概述 679
6.2 分布式程序设计语言CSP 707
6.3 CSP的结构化操作语义 716
6.4 CSP的流语义 727
6.5 TCSP和失败语义 734
6.6 并行程序的公理语义 743
6.7 CSP的公理语义 751
6.8 通信系统演算（CCS） 768
6.9 CCS的操作语义 772
6.10 同步树和通信树 779
6.11 双模拟和行为等价性 786
6.12 SCCS和集合推导语义 797
6.13 CCS的偏序推导语义 802
6.14 CCS的Petri网语义 814
6.15 分布式变迁系统和CCS 820
6.16 CCS的真并发语义 830
6.17 Hennessy-Milner逻辑 848
6.17.1 基本HM逻辑 848
6.17.2 带递归HM逻辑 853
6.18 通信进程代数ACP家族及其静态语义 859
6.18.1 基本进程代数BPA 859
6.18.2 进程代数PA 860
6.18.3 通信进程代数ACP 862
6.18.4 ACP的扩充 864
6.18.5 ACP的最大扩充ACP 870
6.19 动态ACP及其操作语义 873
6.20 ACP的指称语义和双模拟语义 883
6.21 抽象数据类型作为进程代数的代数语义 892
6.22 进程代数并发语义的比较研究 913
第7章 移动通信和移动计算系统的形式语义 927
7.1 概述 927
7.2 π演算及其操作语义 952
7.3 π演算的双模拟语义 975
7.4 进程代数的符号变迁语义 986
7.4.1 CCS型的进程代数的符号语义 986
7.4.2 π演算的（强）符号语义 995
7.4.3 π演算的（弱）符号语义 999
7.5 多维π演算和异步π演算 1001
7.5.1 多维π演算 1001
7.5.2 异步π演算 1010
7.6 安全π演算SPI 1020
7.7 SPI演算的环境敏感双模拟语义 1039
7.8 Appliedπ演算 1059
7.9 Appliedπ演算的符号语义 1072
7.9.1 Delaune，Kremer和Ryan的DAppliedπ演算及其符号语义 1072
7.9.2 Dolev-Yao模型、可达性模型和约束系统 1082
7.9.3 刘佳和林惠民的符号LApplied π演算语义 1085
7.10 对称π演算：x演算和Fusion演算 1092
7.10.1 x演算 1092
7.10.2 Fusion演算 1098
7.11 移动Ambient演算 1106
7.11.1 基本Ambient演算——移动Ambient演算 1107
7.11.2 完整Ambient演算——通信Ambient演算 1116
7.12 Ambeint演算的类型系统 1119
7.13 分布式Ambient演算的双模拟语义 1133
7.14 安全Ambient演算及其双模拟语义 1142
7.14.1 安全Ambient演算SA 1142
7.14.2 带口令的安全Ambient演算SAP 1146
7.15 封装Ambient演算 1155
7.15.1 封装Ambient演算BA 1155
7.15.2 新封装Ambient演算NBA 1161
7.15.3 密封Ambient演算SBA 1165
第8章 非规范进程代数和微观生命系统的形式语义 1169
8.1 概述 1169
8.2 从强化操作语义到因果π演算 1199
8.3 概率进程代数 1210
8.3.1 部分概率进程代数PCCS 1211
8.3.2 全概率进程代数APPA 1226
8.4 性能评估进程代数PEPA 1233
8.5 随机π演算 1252
8.6 含噪π演算 1261
8.7 进程演算的拓扑理论 1275
8.8 进程序列演算CPS 1296
8.8.1 CPS的语法和操作语义 1296
8.8.2 CPS的序列双模拟语义 1299
8.8.3 CPS的特征序列双模拟语义 1309
8.9 CPS的序列极限双模拟 1315
8.9.1 动程的贴近双模拟语义 1315
8.9.2 CPS的极限序列双模拟语义 1318
8.10 Gillespie算法 1331
8.11 π通路演算——分子水平的生物进程代数 1336
8.11.1 关于通路 1336
8.11.2 π通路演算编程信号传导通路 1338
8.11.3 随机π通路演算编程基因调控通路 1345
8.12 κ演算——基于规则的蛋白质相互作用语言 1352
8.12.1 蛋白质相互作用和κ演算 1352
8.12.2 κ演算的操作语义和带钩语义 1360
8.12.3 κ演算的指称语义 1364
8.13 从Gamma模型到化学抽象机 1367
8.13.1 Gamma计算模型 1367
8.13.2 化学抽象机 1368
8.13.3 概率化学抽象机 1375
8.13.4 模糊化学抽象机 1378
8.14 生化抽象机和计算树逻辑 1380
8.15 溶液级建模语言Bio-PEPA 1393
8.16 固定生物膜计算和P系统 1405
8.16.1 基本P系统及其变型 1407
8.16.2 基于通信的P系统 1413
8.16.3 面向DNA计算的H系统和拼接P系统 1414
8.16.4 神经型P系统和尖峰放电型P系统 1419
8.17 基于移动生物膜的BioAmbients演算 1426
8.17.1 BioAmbients演算的基本内容 1426
8.17.2 随机BioAmbients演算 1434
8.18 膜演算语言Brane 1442
8.18.1 膜演算 1442
8.18.2 射影膜演算 1452
第9章 量子语言的形式语义 1459
9.1 概述 1459
9.2 一些基本概念 1494
9.2.1 基于波动力学的量子力学公设 1494
9.2.2 量子力学公设的Hilbert空间表示 1496
9.2.3 量子力学公设的Dirae表示形式 1498
9.3 量子随机存取机、量子伪码及其操作语义 1509
9.3.1 Knill的量子随机存取机QRAM 1509
9.3.2 Nagarajan等的顺序量子随机存取机SQRAM 1512
9.3.3 Adao和Mateus的基于复杂性分析的QRAM设计及其操作语义 1515
9.4 命令式量子语言及其操作语义 1519
9.4.1 命令式量子程序设计语言QC L 1519
9.4.2 命令式量子程序设计语言LanQ的抽象机语义 1526
9.4.3 不确定性命令式量子语言qGCL 1535
9.5 量子λ演算及其类型系统 1537
9.6 函数式量子语言的框图操作语义 1546
9.7 量子程序语义的范畴论诠释 1557
9.8 量子可逆计算和不可逆计算 1575
9.8.1 刻画可逆计算的严格广群语义 1576
9.8.2 刻画不可逆计算的幺半群范畴语义 1579
9.8.3 函数式量子语言QML及其可逆化操作语义 1583
9.8.4 从不可逆计算到可逆计算：pGCL语言的可逆化改造 1583
9.9 函数式量子语言的范畴论指称语义 1588
9.10 量子程序的最弱前置条件语义和公理语义 1599
9.10.1 Hermitian算子作为量子谓词 1599
9.10.2 最弱前置条件语义及其证明规则 1605
9.10.3 量子程序的Hoare公理系统 1609
9.11 量子进程代数的操作语义 1613
9.11.1 量子进程代数QPALg 1613
9.11.2 通信量子进程CQP 1620
9.11.3 量子多项式机器QPM 1624
9.12 量子进程代数的双模拟语义 1630
9.12.1 qCCS1及其量子概率双模拟语义 1630
9.12.2 qCCS2及其渐近双模拟 1640
9.12.3 QPALg的概率分支双模拟 1649
参考文献 1655
中英名词索引 1745
英中名词索引 1801