Trees from Functions as Processes

  • Davide Sangiorgi
  • Xian Xu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


Lévy-Longo Trees and Böhm Trees are the best known tree structures on the λ-calculus. We give general conditions under which an encoding of the λ-calculus into the π-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the call-by-name λ-calculus, showing how the two kinds of tree can be obtained by varying the behavioural equivalence adopted in the π-calculus and/or the encoding. The conditions are presented in the π-calculus but can be adapted to other concurrency formalisms.


Variable Context Process Context Behavioural Equivalence Expansion Relation Initial Abstraction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Arun-Kumar, S., Hennessy, M.: An efficiency preorder for processes. Acta Informatica 29, 737–760 (1992)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Barendregt, H.P.: The Lambda Calculus: Syntax, semantics. North-Holland (1984)Google Scholar
  3. 3.
    Berger, M., Honda, K., Yoshida, N.: Sequentiality and the π-calculus. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 29–45. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Berger, M., Honda, K., Yoshida, N.: Genericity and the pi-calculus. Acta Informatica 42(2-3), 83–141 (2005)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Demangeon, R., Honda, K.: Full abstraction in a subtyped pi-calculus with linear types. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 280–296. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    Dezani-Ciancaglini, M., Giovannetti, E.: From Bohm’s theorem to observational equivalences: an informal account. ENTCS 50(2), 83–116 (2001)Google Scholar
  7. 7.
    Hirschkoff, D., Madiot, J.M., Sangiorgi, D.: Duality and i/o-types in the π-calculus. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 302–316. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  8. 8.
    Milner, R.: Functions as processes. Mathematical Structures in Computer Science 2(2), 119–141 (1992)CrossRefzbMATHMathSciNetGoogle Scholar
  9. 9.
    Milner, R.: Communicating and Mobile Systems: The π-Calculus. CUP (1999)Google Scholar
  10. 10.
    Plotkin, G.D.: T ω as a universal domain. Journal of Computer and System Sciences 17, 209–236 (1978)CrossRefzbMATHMathSciNetGoogle Scholar
  11. 11.
    Sangiorgi, D.: Lazy functions and mobile processes. In: Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 691–720. MIT Press (2000)Google Scholar
  12. 12.
    Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. CUP (2001)Google Scholar
  13. 13.
    Scott, D.: Data types as lattices. SIAM Journal on Computing 5(3), 522–587 (1976)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Yoshida, N., Honda, K., Berger, M.: Linearity and bisimulation. Journal of Logic and Algebraic Programming 72(2), 207–238 (2007)CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Davide Sangiorgi
    • 1
  • Xian Xu
    • 2
  1. 1.University of Bologna/INRIABolognaItaly
  2. 2.East China University of Science and TechnologyShanghaiChina

Personalised recommendations