Abstract
FM (Fraenkel Mostowski) techniques are an approach to metaprogramming on syntax in the presence of binding. We develop novel FM theory and with it develop theory of π-calculus syntax and its operational semantics. Technicalities of name binding and also of name generation in transitions are smoothly handled.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Bibliography
Gerard Berry and Gerard Boudol. The chemical abstract machine. In Proceedings of the seventeenth annual ACM symposium on Principles of programming languages, pages 81–94, New York, NY, USA, 1990. ACM Press.
R. Bruni, F. Honsell, M. Lenisa, and M. Miculan. Modeling fresh names in pi-calculus using abstractions. Technical Report 21/2002, Dipartimento di Matematica e Informatica, University of Udine (Italy), April 2002.
A. Bucalo, M. Hofmann, F. Honsell, M. Miculan, and I. Scagnetto. Consistency of the theory of contexts, 2001.
Gian Luca Cattani and Peter Sewell. Models for name-passing processes: Interleaving and causal. In Logic in Computer Science, pages 322–332, 2000.
Gian Luca Cattani, Ian Stark, and Glynn Winskel. Presheaf models for the pi-calculus. In E[ugenio] Moggi and G[iuseppe] Rosolini, editors, Proceedings of the 7th International Conference on Category Theory and Computer Science (Santa Margherita Ligure, Italy, September 4–6, 1997),volume 1290 of LNCS,pages 106–126. Springer, 1997.
Marcelo Fiore and Daniele Tari. Semantics of name and value passing. In Proc. 16 th LICS Conf., pages 93–104. IEEE, Computer Society Press, 2001.
Marcelo Fiore, Eugenio Moggi, and Davide Sangiorgi. A fully-abstract model for the 7r-calculus (extended abstract). In Eleventh Annual Symposium on Logic in Computer Science (LICS) (New Brunswick, New Jersey),pages 43–54. IEEE, Computer Society Press, July 1996.
M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In 14th Annual Symposium on Logic in Computer Science, pages 193–202. IEEE Computer Society Press, Washington, 1999.
FreshML. FreshML homepage, 2003. http://vvv.freshml.org.
M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13: 341–363, 2001.
Murdoch J. Gabbay. A Theory of Inductive Definitions with alphaEquivalence. PhD thesis, Cambridge, UK, 2000.
Daniel Hirschkoff. A full formalization of pi-calculus theory in the Calculus of Constructions. In E. Gunter and A. Felty, editors, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’97), pages 153–169, Murray Hill, New Jersey, August 1997.
Daniel Hirschkoff. Mis en oeuvre de preuves de bisimulation. PhD thesis, École Nationale des Ponts et des Changes (ENPC), January 1999. In French.
Furio Honsell, Marino Miculan, and Ivan Scagnetto. 7r-calculus in (co)inductive type theory. Theoretical Computer Science, 253(2): 239–285, 2001.
M. Martin and D. Gordon. A calculus for cryptographic protocols: the spi calculus. Technical Report SRC-RR-149, Internationales Begegnungs und Forschungszentrum Schloss Dagstuhl, Germany, 1993.
Robin Milner, Joachim Parrow, and David Walker A calculus of mobile processes, II. Information and Computation, 100(1): 41–77, September 1992.
Ugo Montanari and Marco Pistore. An introduction to history dependent automata. In Andrew Gordon, Andrew Pitts, and Carolyn Talcott, editors, Conference Record of the Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II, Stanford University, December 8–12, 1997), volume 10 of ENTCS. Elsevier Science Publishers, 1997.
Joachim Parrow. An introduction to the pi-calculus. In Jan Bergstra, Alban Ponse, and Scott Smolka, editors, Handbook of Process Algebra, pages 479–543. Elsevier Science, 2001.
A. M. Pitts and M. J. Gabbay. A metalanguage for programming with bound names modulo renaming. In R. Backhouse and J. N. Oliveira, editors, Mathematics of Program Construction. 5th International Conference, MPC2000, Ponte de Lima, Portugal, July 2000. Proceedings, volume 1837 of Lecture Notes in Computer Science, pages 230–255. Springer-Verlag, Heidelberg, 2000.
A. M. Pitts. Nominal logic, a first order theory of names and binding. Information and Computation, 2001. To appear. (A preliminary version appeared in the Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001), LNCS 2215, Springer-Verlag, 2001, pp 219–242.).
M. R. Shinwell, A. M. Pitts, and M. J. Gabbay. FreshML: Programming with binders made simple. In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden. ACM Press, August 2003.
C. Urban, A. M. Pitts, and M. J. Gabbay. Nominal unification. In M. Baaz, editor, Computer Science Logic and 8th Kurt Gödel Colloquium (CSL’03 zhaohuan KG C), Vienna, Austria. Proccedings, Lecture Notes in Computer Science. Springer-Verlag, Berlin, 2003.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Gabbay, M.J. (2003). The π-Calculus in FM. In: Kamareddine, F.D. (eds) Thirty Five Years of Automating Mathematics. Applied Logic Series, vol 28. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0253-9_10
Download citation
DOI: https://doi.org/10.1007/978-94-017-0253-9_10
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-6440-0
Online ISBN: 978-94-017-0253-9
eBook Packages: Springer Book Archive