文档介绍:鲁棒灰箱演算的类型系统和代数性质研究博士生:管旭东导师:尤晋元上海交大计算机科学与工程系分布计算技术中心2002 . 6
博士论文答辩
2002-6
博士论文答辩- 鲁棒灰箱演算
. 2 .
内容提要
1. 论文的背景
2. 灰箱演算,研究ROAM的原因
3. 演化类型系统
4. ROAM的进程等价性
5. 演算的翻译及证明
6. 总结论文的创新处
2002-6
博士论文答辩- 鲁棒灰箱演算
. 3 .
论文的背景
移动计算
硬件移动、软件移动
网络的广域化、全球化
从技术到理论支持
从程序设计理论(programming language theory)角度
寻求支持并发(concurrency)、分布(distribution)、移动(mobility)S,CSP,,,join,ambient,seal,...)
目标:作为支持全球性移动计算编程语言的理论基础
2002-6
博士论文答辩- 鲁棒灰箱演算
. 4 .
相关研究领域
本论文有关灰箱演算(ambient calculus)的研究工作,属于:
程序设计理论(并发、分布、移动)
进程代数
相关研究领域:
OS (distributed/mobile): OS support for Java and mobile agent technology
TCS: type theory and semantics
Security - Wide work, software mobility
2002-6
博士论文答辩- 鲁棒灰箱演算
. 5 .
灰箱演算的相关工作
支持分布、移动的形式化模型,除了Ambient, 还有:
dist: Sekiguchi,., 1997,
D: Henessey, ., 1998, U. Sussex
1l : Amadio, 1997
Distributed-: Sewell, 1998, Cambridge
D-join: , ., 1996, INRIA
Seal: Vitek, , 1999, U. Purdue
...
2002-6
博士论文答辩- 鲁棒灰箱演算
. 6 .
内容提要
1. 论文的背景
2. 灰箱演算,研究ROAM的原因
3. 演化类型系统
4. ROAM的进程等价性
5. pi演算的翻译及证明
6. 总结论文的创新处
2002-6
博士论文答辩- 鲁棒灰箱演算
. 7 .
MA在提出后迅速成为研究热点
Cardelli & Gordon: “Mobile Ambients”
Digital Research => Microsoft Research
会议:FoSSaCS’98
期刊:puter Science, 2000
后续研究:
Ambient有关的研究论文:50多篇
FoSSaCS’98的引用数:200左右(./, 2002-05) (SCI引用数: 50左右)
欧盟:2002启动FET-
2002-6
博士论文答辩- 鲁棒灰箱演算
. 8 .
MA用三个原语来描述移动计算
cs[mail[out cs . in lib . Body]] | lib[open mail]
lib
open mail
cs
out cs . in lib . Body
mail
2002-6
博士论文答辩- 鲁棒灰箱演算
. 9 .
out 使一个灰箱移出其父灰箱
lib
open mail
cs
out cs . in lib . Body
mail
lib
in lib . Body
mail
open mail
cs
2002-6
博士论文答辩- 鲁棒灰箱演算
. 10 .
in 使一个灰箱移进另一个同层灰箱
cs
in lib . Body
mail
lib
open mail
Body
mail
lib
open mail
cs