Investigating the Logical Aspects of the Pi-calculus

• Autorzy: Bernard N.
• Języki publikacji: PL

Abstrakty

EN

The relations between the p-calculus and logic have been less extensively studied than for the l-calculus. We give an account on what can be found in the literature, in two distinct directions: model-checking, and typing. We propose a Curry-Howard correspondence taking into account the dynamic properties of the p-calculus. This is a first presentation of a work in progress.

Słowa kluczowe

EN

pi-calculus; model checking; mi-logic; proof theory; Curry-Howard correspondence

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Schedae Informaticae
• Rocznik: 2003
• Tom: Vol. 12
• Strony: 57--66
• Opis fizyczny: Bibliogr. 20 poz.

Twórcy

autor

Bernard N.

• LAMA-Universite de Savoie, Campus Scientifique, F-73376 Le Bourget-du-Lac,

Bibliografia

• [1] Abadi M., Gordon A.D.; A calculus for cryptographic protocols: The Spi calculus, Fourth ACM Conference on Computer and Communications Security, ACM Press, 1997, pp. 36-47.
• [2] Berger M., Honda K., Yoshida N.; Sequentiality and the pi-calculus. International Conference on Typed Lambda Calculi and Applications (TCLA 2001, Kraków, Poland), Lecture Notes in Computer Science, Springer-Verlag, Vol. 2044, 2001, pp. 29-45.
• [3] Bernard N., Dumond Y.; Specification en pi-calcul de Vetude de cas relative au contróle d'acces, AFADL’2000, LSR/IMAG - BP 72 38402 Saint-Martin d’Heres Cedex-Grenoble-France, January 2000, LSR/IMAG, LSR/IMAG.
• [4] Boudol G.; The TT-calculus in direct style. Higher-Order and Symbolic Computation, Vol. 11(2), 1998, pp. 177-185.
• [5] Cardelli L., Gordon A.D.; Mobile ambients, in: M. Nivat, (ed.), Foundations of Software Science and Computational Structures, Lecture Notes in Computer Science, Springer-Verlag, Vol. 1378, 1998, pp. 140-155.
• [6] Dam M.; Model checking mobile processes, Lecture Notes in Computer Science, Vol. 715, 1993, pp. 22-36.
• [7] Emerson E.A., Clarke E.M.; Characterizing correctness properties of parallel programs using fixpoints, in: J.W. de Bakker and J. van Leeuwen, (eds.), Automata, Languages and Programming, 7th Colloquium, Lecture Notes in Computer Science, Noordweijkerhout, The Netherland, 14-18 July 1980, Springer- Verlag, Vol. 85, pp. 169-181.
• [8] Fournet C.; The .Join-Calculus: a Calculus for Distributed Mobile Programming, Ph.D. thesis, Ecole Polytechnique, 1998.
• [9] Gordon A.D.; Notes on nominal calculi for security and mobility, Lecture Notes in Computer Science, Vol. 2171, 2001, pp. 262-330.
• [10] Holzmann G.J.; The model checker spin. IEEE Trans, on Software Engineering. Special issue on Formal Methods in Software Practice, May 1997, Vol. 23(5), pp. 279-295.
• [11] LISI/ENSMA: Approches Formelles dans l'Assistance au Développement de Logiciels (Proceedings of AFADL '98). Téléport2 - Avenue 1 - BP109 - 86960 FUTUROSCOPE Cedex, October 1998.
• [12]Milner R.; Functions as processes, Mathematical Structures in Computer Science, Vol. 2, 1992, pp. 119-141.
• [13] Milner R., Parrow J., Walker D.; A calculus of mobile processes (Parts I and II), Information and Computation, Vol. 100, 1992, pp. 1-77.
• [14] Milner R.; The polyadic-K-calculus: a tutorial. LFCS Report Series ECS-LFCS- 91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, UK, Heidelberg, October 1991.
• [15] Needham R.M.; Names, in: S. Mullender, (ed.), Distributed Systems, Chapter 5, 1989, pp. 89-102.
• [16] Orava F., Parrow J.; An algebraic verification of a mobile network, Formal Aspects of Computing, Vol. 4(6), 1992, pp. 497-543.
• [17] Sangiorgi D.; Expressing Mobility in Process Algebras: First-Order and Higher- Order Paradigms, Ph.D. thesis, Computer Science Dept., University of Edinburgh, May 1993.
• [18] Sangiorgi D., Walker D.; The π-calculus: a Theory of Mobile Processes, Cambridge University Press, 2001.
• [19] Victor B., Möller F.; The Mobility Workbench - A tool for the π-calculus, in: D. Dill, (ed.), Computer Aided Verification (Proc. of CAV’94), Lecture Notes in Computer Science, Springer-Verlag, Vol. 818, 1994, pp. 428-440.
• [20] Yoshida N., Berger M., Honda K.; Strong normalisation in the π-calculus, 16th Annual IEEE Symposium on Logic in Computer Science (LICS ’01), Washington-Brussels-Tokyo, June 2001, pp. 311-322.