\(\pi\)-calculus in (Co)inductive-type theory.

*(English)*Zbl 0956.68095Summary: We present a large and we think also significant case study in computer assisted formal reasoning. We start by giving a higher-order abstract syntax encoding of \(\pi\)-calculus in the higher-order inductive/coinductive-type theories CIC and \(CC^{(Co)Ind}.\) This encoding gives rise to a full-fledged proof editor/proof assistant for the \(\pi\)-calculus, once we embed it in Coq, an interactive proof-development environment for \(CC^{(Co)Ind}.\) Using this computerized assistant we prove formally a substantial chapter of the theory of strong late bisimilarity, which amounts essentially to Section 2 of A calculus of mobile processes by Milner, Parrow, and Walker. This task is greatly simplified by the use of higher-order syntax. In fact, not only we can delegate conveniently to the metalanguage \(\alpha\)-conversion and substitution, but, introducing a suitable axiomatization of the theory of contexts, we can accommodate also the machinery for generating new names. The axiomatization we introduce is quite general and should be easily portable to other formalizations based on higher-order syntax. The use of coinductive types and corresponding tactics allows to give alternative, and possibly more natural, proofs of many properties of strong late bisimilarity, w.r.t. those originally given by Milner, Parrow, and Walker.

##### MSC:

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

##### Keywords:

higher-order abstract syntax; \(\pi\)-calculus; proof checking; logical frameworks; typed \(\pi\)-calculus
PDF
BibTeX
XML
Cite

\textit{F. Honsell} et al., Theor. Comput. Sci. 253, No. 2, 239--285 (2001; Zbl 0956.68095)

Full Text:
DOI

**OpenURL**

##### References:

[1] | Avron, A.; Honsell, F.; Mason, I.A.; Pollack, R., Using typed lambda calculus to implement formal systems on a machine, J. automat. reason., 9, 309-354, (1992) · Zbl 0784.68072 |

[2] | The Coq Proof Assistant Reference Manual - Version 6.2, INRIA, May 1998, Available at . |

[3] | Coquand, T., Infinite objects in type theory, (), 62-78 |

[4] | Coquand, T.; Huet, G., The calculus of constructions, Inform. and control, 76, 95-120, (1988) · Zbl 0654.03045 |

[5] | Cornes, C.; Terrasse, D., Automating inversion and inductive predicates in coq, (), 85-104 · Zbl 1407.68433 |

[6] | J. Despeyroux, A. Felty, A. Hirschowitz, Higher-order syntax in Coq, Proc. TLCA’95, Lecture Notes in Computer Science, vol. 905, Springer, Berlin, 1995. · Zbl 1063.68650 |

[7] | J. Despeyroux, F. Pfenning, C. Schürmann, Primitive recursion for higher order abstract syntax, CMU-CS-96-172, School of Computer Science, Carnegie Mellon University, Pittsburgh, August 1996. |

[8] | M. Felchero, Sistemi di transizione in teoria dei tipi coinduttivi, Laurea’s Thesis, Università di Udine, Italy, July 1996 (in Italian). |

[9] | H. Geuvers, Inductive and coinductive types with iteration and recursion. Available at , June 1992. |

[10] | Giménez, E., Codifying guarded recursion definitions with recursive schemes, proc. TYPES’94, lecture notes in computer science, vol. 996, (1995), Springer Berlin |

[11] | Giménez, E., An application of co-inductive types in coqverification of the alternating bit protocol, (), 134-152 · Zbl 1407.68435 |

[12] | Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, J. ACM, 40, 1, 143-184, (1993) · Zbl 0778.03004 |

[13] | Hirschkoff, D., Bisimulation proofs for the \(π\)-calculus in the calculus of constructions, proc. TPHOL’97, lecture notes in computer science, vol. 1275, (1997), Springer Berlin |

[14] | Honsell, F.; Lenisa, M.; Montanari, U.; Pistore, M., Final semantics for the \(π\)-calculus, proc. PROCOMET’98, (1998), IFIP and Chapman & Hall London |

[15] | Honsell, F.; Miculan, M., A natural deduction approach to dynamic logics, (), 165-182 · Zbl 1434.03084 |

[16] | M. Hofmann, Semantical analysis of higher-order abstract syntax, Proc. 14th LICS, IEEE, New York, 1999. |

[17] | M. Lenisa, Themes in final semantics, Ph.D. Thesis, Dipartimento di Informatica, Università di Pisa, Italy, March 1998. |

[18] | P. Martin-Löf, On the meaning of the logical constants and the justifications of the logic laws, TR 2, Dip. di Matematica, Università di Siena, 1985. |

[19] | R. McDowell, D. Miller, A logic for reasoning with higher-order abstract syntax, Proc. 12th LICS, IEEE, New York, 1997. |

[20] | Melham, T.F., A mechanized theory of the \(π\)-calculus in HOL, Nordic J. comput., 1, 1, 50-76, (1994) |

[21] | M. Miculan, The expressive power of structural operational semantics with explicit assumptions, in: Proc. TYPES’93 Lecture Notes in Computer Science, vol. 806, Springer, Berlin, 1994, pp. 292-320. |

[22] | M. Miculan, Encoding logical theories of programs, Ph.D. Thesis, Dipartimento di Informatica, Università di Pisa, Italy, March 1997. |

[23] | R. Milner, The polyadic \(π\)-calculus: a tutorial, in: Logic and Algebra of Specification, NATO ASI Series F, vol. 94, Springer, Berlin, 1993. |

[24] | R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, Tech. Rep. ECS-LFCS-89-85, Dept. of Computer Science, Univ. of Edinburgh, June 1989. · Zbl 0752.68037 |

[25] | Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, Inform. and comput., 100, 1, 1-77, (1992) · Zbl 0752.68037 |

[26] | Milner, R.; Parrow, J.; Walker, D., Modal logics for mobile processes, Theoret. comput. sci., 114, 1, 149-171, (1993) · Zbl 0778.68033 |

[27] | T. Nipkow, L.C. Paulson, Isabelle-91 - System abstract, Proc. CADE 11, Lecture Notes in Computer Science, vol. 607, Springer, Berlin, 1992, pp. 673-676. |

[28] | Nordström, B.; Petersson, K.; Smith, J.M., Programming in martin-Löf’s type theory: an introduction, (1990), OUP Oxford |

[29] | C. Paulin-Mohring, Inductive definitions in the system Coq; rules and properties, Proc. TLCA’94, Lecture Notes in Computer Science, vol. 664, Springer, Berlin, 1993, pp. 328-345. · Zbl 0844.68073 |

[30] | F. Pfenning, C. Elliott, Higher-order abstract syntax, Proc. ACM SIGPLAN ’88, ACM, New York, June 1988, pp. 199-208. |

[31] | R. Pollack, The theory of LEGO, Ph.D. Thesis, Univ. of Edinburgh, 1994. |

[32] | A. Rossi, Tipi di dati coinduttivi: i reali, Laurea’s Thesis, Università di Udine, Italy, 1994. |

[33] | Sangiorgi, D., A theory of bisimulation for the \(π\)-calculus, Acta inform., 33, 69-97, (1996) · Zbl 0835.68072 |

[34] | I. Scagnetto, Rappresentazione di algebre di processi in logical frameworks, Laurea’s Thesis, Università di Udine, March 1997 (in italian). |

[35] | Schroeder-Heister, P., A natural extension of natural deduction, J. symbolic logic, 49, 4, 1284-1300, (1984) · Zbl 0574.03045 |

[36] | Proc. TYPES’93, Lecture Notes in Computer Science, vol. 806, Springer, Berlin, 1994. |

[37] | Proc. TYPES’95, Lecture Notes in Computer Science, vol. 1158, Springer, Berlin, 1996. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.