iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/978-3-031-62645-6_7
Leaf-First Zipper Semantics | SpringerLink
Skip to main content
Springer Nature Link
Log in

Leaf-First Zipper Semantics

  • Conference paper
  • First Online:
Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14678))

  • 108 Accesses

Abstract

Biernacka et al. recently proposed zipper semantics, a semantics format from which sound and complete abstract machines for non-deterministic languages can be automatically derived. We present a new style of zipper semantics, called leaf-first, in which we express the semantics of two extensions of HO\(\pi \), a higher-order version of the \(\pi \)-calculus: one with passivation and the other with join patterns. The leaf-first style is better suited than the original one to express phenomena occurring in process calculi semantics such as scope extrusion, which is observable with passivation and complex with join patterns.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    As bound variables in a join pattern are distinct, \(\theta _{1}\) and \(\theta _{2}\) have disjoint domains.

References

  1. Bidinger, P., Schmitt, A., Stefani, J.-B.: An abstract machine for the kell calculus. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 31–46. Springer, Heidelberg (2005). https://doi.org/10.1007/11494881_3

    Chapter  Google Scholar 

  2. Biernacka, M., Biernacki, D., Lenglet, S., Schmitt, A.: Non-deterministic abstract machines. Tech. Rep. 9475, Inria (2022), available at https://hal.inria.fr/hal-03545768

  3. Biernacka, M., Biernacki, D., Lenglet, S., Schmitt, A.: Non-deterministic abstract machines. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland. LIPIcs, vol. 243, pp. 7:1–7:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

    Google Scholar 

  4. Bugliesi, M., Crafa, S., Merro, M., Sassone, V.: Communication and mobility control in boxed ambients. Inf. Comput. 202(1), 39–86 (2005)

    Google Scholar 

  5. Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FoSSaCS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053547

    Chapter  Google Scholar 

  6. Castagna, G., Vitek, J., Nardelli, F.Z.: The seal calculus. Inf. Comput. 201(1), 1–54 (2005)

    Google Scholar 

  7. Danvy, O.: From reduction-based to reduction-free normalization. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 66–164. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04652-0_3

    Chapter  Google Scholar 

  8. Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235–271 (1992)

    Google Scholar 

  9. Fessant, F.L.: JoCaml: conception et implémentation d’un langage à agents mobiles. Ph.D. thesis, École polytechnique (2001)

    Google Scholar 

  10. Fessant, F.L., Maranget, L.: Compiling join-patterns. In: Nestmann, U., Pierce, B.C. (eds.) 3rd International Workshop on High-Level Concurrent Languages, HLCL 1998, Satellite Workshop of CONCUR 1998, Nice, France, September 12, 1998, pp. 205–224. No. 16(3) in Electronic Notes in Theoretical Computer Science, Elsevier (1998). https://doi.org/10.1016/S1571-0661(04)00143-4, https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/16/issue/3

  11. Fournet, C., Gonthier, G.: The reflexive CHAM and the join-calculus. In: Boehm, H., Jr., G.L.S. (eds.) Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, pp. 372–385. ACM Press (1996)

    Google Scholar 

  12. Gardner, P., Laneve, C., Wischik, L.: The fusion machine. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 418–433. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45694-5_28

    Chapter  Google Scholar 

  13. Germain, F., Lacoste, M., Stefani, J.: An abstract machine for a higher-order distributed process calculus. Electron. Notes Theor. Comput. Sci. 66(3), 145–169 (2002)

    Google Scholar 

  14. Giannini, P., Sangiorgi, D., Valente, A.: Safe ambients: abstract machine and distributed implementation. Sci. Comput. Program. 59(3), 209–249 (2006)

    Google Scholar 

  15. Godskesen, J.C., Hildebrandt, T., Sassone, V.: A calculus of mobile resources*. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 272–287. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45694-5_19

    Chapter  Google Scholar 

  16. Hirschkoff, D., Pous, D., Sangiorgi, D.: An efficient abstract machine for safe ambients. J. Log. Algebraic Methods Program. 71(2), 114–149 (2007)

    Google Scholar 

  17. Lenglet, S., Schmitt, A.: Leaf-first zipper semantics (2024), available at https://inria.hal.science/hal-04537440

  18. Lenglet, S., Schmitt, A., Stefani, J.: Characterizing contextual equivalence in calculi with passivation. Inf. Comput. 209(11), 1390–1433 (2011)

    Google Scholar 

  19. Lopes, L., Silva, F., Vasconcelos, V.T.: A virtual machine for a process calculus. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 244–260. Springer, Heidelberg (1999). https://doi.org/10.1007/10704567_15

    Chapter  Google Scholar 

  20. Nestmann, U.: On the expressive power of joint input. In: Castellani, I., Palamidessi, C. (eds.) Fifth International Workshop on Expressiveness in Concurrency, EXPRESS 1998, Satellite Workshop of CONCUR 1998, Nice, France, September 7, 1998, pp. 145–152. No. 16(2) in Electronic Notes in Theoretical Computer Science, Elsevier (1998). https://doi.org/10.1016/S1571-0661(04)00123-9, https://doi.org/10.1016/S1571-0661(04)00123-9

  21. Phillips, A., Cardelli, L.: A correct abstract machine for the stochastic pi-calculus. In: Concurrent Models in Molecular Biology (2004)

    Google Scholar 

  22. Phillips, A., Yoshida, N., Eisenbach, S.: A distributed abstract machine for boxed ambient calculi. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 155–170. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24725-8_12

    Chapter  Google Scholar 

  23. Plotkin, G.D.: A structural approach to operational semantics. Tech. Rep. FN-19, DAIMI, Department of Computer Science, Aarhus University, Aarhus, Denmark (1981)

    Google Scholar 

  24. Sangiorgi, D.: Bisimulation in higher-order process calculi. In: Olderog, E. (ed.) Programming Concepts, Methods and Calculi, Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET ’94) San Miniato, Italy, 6-10 June, 1994. IFIP Transactions, vol. A-56, pp. 207–224. North-Holland (1994)

    Google Scholar 

  25. Sangiorgi, D., Walker, D.: The Pi-Calculus - a theory of mobile processes. Cambridge University Press (2001)

    Google Scholar 

  26. Schmitt, A., Stefani, J.-B.: The kell calculus: a family of higher-order distributed process calculi. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 146–178. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31794-4_9

    Chapter  Google Scholar 

  27. Turner, D.: The polymorphic pi-calculus:theory and implementation. Ph.D. Thesis, University of Edinburgh (1995)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Lorraine, Nancy, France

    Sergueï Lenglet

  2. Université Sorbonne Paris Nord, Villetaneuse, France

    Sergueï Lenglet

  3. INRIA, Rennes, France

    Alan Schmitt

Authors
  1. Sergueï Lenglet
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alan Schmitt
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sergueï Lenglet .

Editor information

Editors and Affiliations

  1. Eindhoven University of Technology, Eindhoven, The Netherlands

    Valentina Castiglioni

  2. University of Malta, Msida, Malta

    Adrian Francalanza

Rights and permissions

Reprints and permissions

Copyright information

© 2024 IFIP International Federation for Information Processing

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lenglet, S., Schmitt, A. (2024). Leaf-First Zipper Semantics. In: Castiglioni, V., Francalanza, A. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2024. Lecture Notes in Computer Science, vol 14678. Springer, Cham. https://doi.org/10.1007/978-3-031-62645-6_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-62645-6_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-62644-9

  • Online ISBN: 978-3-031-62645-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation