| 摘要 | 第1-7页 |
| ABSTRACT(英文摘要) | 第7-12页 |
| 第一章 引言 | 第12-26页 |
| §1.1 背景 | 第12-14页 |
| §1.1.1 进程演算的一般背景 | 第12-13页 |
| §1.1.2 Mobility | 第13-14页 |
| §1.2 动机和贡献 | 第14-23页 |
| §1.3 论文章节安排 | 第23-26页 |
| 第二章 预备知识 | 第26-38页 |
| §2.1 高阶进程演算概览 | 第26-33页 |
| §2.1.1 Plain CHOCS | 第26-27页 |
| §2.1.2 高阶π演算 | 第27-31页 |
| §2.1.3 线性高阶π演算 | 第31-33页 |
| §2.2 互模拟基础知识简介 | 第33-38页 |
| §2.2.1 强与弱互模拟 | 第33-34页 |
| §2.2.2 迟和早互模拟 | 第34页 |
| §2.2.3 同余 | 第34-35页 |
| §2.2.4 互模拟Up-to | 第35-38页 |
| 第三章 带mismatch的高阶π演算 | 第38-60页 |
| §3.1 简介 | 第38页 |
| §3.2 带mismatch的高阶π演算 | 第38-45页 |
| §3.2.1 语法 | 第38-42页 |
| §3.2.2 语义 | 第42-44页 |
| §3.2.3 线性片段 | 第44-45页 |
| §3.3 互模拟 | 第45-60页 |
| §3.3.1 互模拟定义 | 第46-52页 |
| §3.3.2 等价关系 | 第52-56页 |
| §3.3.3 同余性 | 第56-60页 |
| 第四章 开弱高阶互模拟的特征刻画 | 第60-72页 |
| §4.1 带前缀进程和剩余进程间的关系 | 第60-66页 |
| §4.1.1 高阶输入 | 第61-63页 |
| §4.1.2 高阶输出 | 第63-66页 |
| §4.2 局部环境中的同余 | 第66-72页 |
| §4.2.1 局部同余 | 第68-69页 |
| §4.2.2 更多技术引理 | 第69-72页 |
| 第五章 公理化 | 第72-98页 |
| §5.1 公理系统 | 第74-77页 |
| §5.2 范式 | 第77-79页 |
| §5.3 Saturation性质 | 第79-82页 |
| §5.4 完备性 | 第82-90页 |
| §5.5 讨论 | 第90-96页 |
| §5.5.1 定义 | 第90-91页 |
| §5.5.2 一些性质 | 第91-93页 |
| §5.5.3 公理系统 | 第93-96页 |
| §5.6 小结 | 第96-98页 |
| 第六章 在高阶演算中表达一阶π演算 | 第98-126页 |
| §6.1 简介 | 第98-99页 |
| §6.2 基本定义 | 第99-107页 |
| §6.2.1 FOPi | 第99-101页 |
| §6.2.2 Plain CHOCS | 第101-104页 |
| §6.2.3 Indexed Plain CHOCS | 第104-107页 |
| §6.3 编码策略 | 第107-113页 |
| §6.3.1 Wire的刻画 | 第109-113页 |
| §6.4 索引技术下的编码策略 | 第113-121页 |
| §6.4.1 带索引的编码策略 | 第114页 |
| §6.4.2 刻画indexed wire | 第114-118页 |
| §6.4.3 全抽象相关性质 | 第118-121页 |
| §6.5 讨论及工作展望 | 第121-124页 |
| §6.6 小结 | 第124-126页 |
| 第七章 线性高阶π演算中局部互模拟的再研究 | 第126-156页 |
| §7.1 简介 | 第126-127页 |
| §7.2 线性高阶π演算 | 第127-134页 |
| §7.2.1 语法 | 第127-129页 |
| §7.2.2 语义 | 第129-132页 |
| §7.2.3 互模拟 | 第132-134页 |
| §7.3 简化局部互模拟 | 第134-154页 |
| §7.3.1 局部线性互模拟 | 第135页 |
| §7.3.2 刻画局部线性互模拟 | 第135-147页 |
| §7.3.3 与局部互模拟性的一致性 | 第147-149页 |
| §7.3.4 关于一阶受限输出 | 第149-151页 |
| §7.3.5 逼近局部互模拟 | 第151-154页 |
| §7.4 小结 | 第154-156页 |
| 第八章 线性高阶π演算中的逻辑刻画 | 第156-176页 |
| §8.1 简介 | 第156-158页 |
| §8.2 线性高阶π演算的重新形式化 | 第158-165页 |
| §8.2.1 语法 | 第158-159页 |
| §8.2.2 语义 | 第159-162页 |
| §8.2.3 互模拟 | 第162-165页 |
| §8.3 逻辑 | 第165-170页 |
| §8.3.1 特征公式 | 第167-168页 |
| §8.3.2 刻画定理 | 第168-170页 |
| §8.4 讨论 | 第170-174页 |
| §8.4.1 Q-开互模拟 | 第171-172页 |
| §8.4.2 逻辑刻画的再研究 | 第172-174页 |
| §8.5 展望 | 第174-175页 |
| §8.6 小结 | 第175-176页 |
| 第九章 总结与展望 | 第176-180页 |
| 参考文献 | 第180-186页 |
| 索引 | 第186-190页 |
| 图列表 | 第190-191页 |
| 致谢 | 第191-192页 |
| 论文列表 | 第192页 |