The λ-calculus in the π-calculus

被引：5
作者：
Cai, Xiaojuan [1 ]
Fu, Yuxi
机构：
[1] Shanghai Jiao Tong Univ, Dept Comp Sci, BASICS, Shanghai 200240, Peoples R China
来源：
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE | 2011年 / 21卷 / 05期
基金：
美国国家科学基金会;
关键词：
D O I：
10.1017/S0960129511000260
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A general approach is proposed for transforming objects to methods on the fly in the framework of the pi-calculus. The power of the approach is demonstrated by applying it to generate an encoding of the full lambda calculus in the pi-calculus. The encoding is proved to preserve and reflect beta reduction, and is shown to be fully abstract with respect to Abramsky's applicative bisimilarity.
引用
收藏
页码：943 / 996
页数：54
相关论文
共 34 条
  • [1] A calculus for cryptographic protocols: The spi calculus
    Abadi, M
    Gordon, AD
    [J]. INFORMATION AND COMPUTATION, 1999, 148 (01) : 1 - 70
  • [2] Abramsky S., 1990, LAZY LAMBDA CALCULUS, P65
  • [3] Modelling IP mobility
    Amadio, RM
    Prasad, S
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2000, 17 (01) : 61 - 99
  • [4] Spi calculus translated to π-calculus preserving may-tests
    Baldamus, M
    Parrow, J
    Victor, B
    [J]. 19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 22 - 31
  • [5] Barendregt H. P., 1984, LAMBDA CALCULUS ITS
  • [6] BOUDOL G, 1992, 1702 INRIA SOPH ANT
  • [7] FU Y, 2010, VALUE PASSING CALCUL
  • [8] FU Y, 2010, NAME PASSING CALCULU
  • [9] Fu Y, 2010, INT CONF BIOINFORM
  • [10] On the expressiveness of interaction
    Fu, Yuxi
    Lu, Hao
    [J]. THEORETICAL COMPUTER SCIENCE, 2010, 411 (11-13) : 1387 - 1451
1234