A full formalisation of π-calculus theory in the calculus of constructions

1. S. Abramsky. The lazy lambda calculus. Research Topics in Functional Programming, pages 65–116, 1989.

   Google Scholar 

2. R. Amadio, L Castellani, and D. Sangiorgi. On bisimulations for the asynchronous π-calculus. In CONCUR '96, number 1119 in LNCS, 1996.

   Google Scholar 

3. O. Ait-Mohamed. Vérification de I'équivalence du π-calcul dans HOL. Rapport de recherche 2412, INRIA-Lorraine, November 1994. (In French).

   Google Scholar 

4. O. Ait-Mohamed. PIC: A proof checker for the π-calculus in Higher Order Logic. Technical report, INRIA-Lorraine, 1995.

   Google Scholar 

5. Simon J. Ambler. A de Bruijn notation for the π-calculus. Technical Report 569, Dept. of Computer Science, Queen Mary and Westfield College, London, May 1991

   Google Scholar 

6. B. Barras, S. Boutin, C. Cornes, J. Courant, JC. Filliâtre, E. Gimenez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual. Projet Coq, INRIA Rocquencourt / CNRS-ENS Lyon, 1996.

   Google Scholar 

7. J. Bertot, Y. Bertot, Y. Coscoy, H. Goguen, and F. Montagnac. User Guide to the CtCoq Proof Environment. INRIA, Sophia-Antipolis, February 1996.

   Google Scholar 

8. Y. Bertot, G. Kahn, and L. Théry. Proof by pointing. In Proceedings of STACS, LNCS, Sendai (Japan), April 1994.

   Google Scholar 

9. S. Boutin. Using reflection to build efficient and certified decision procedures. Unpublished — available at http://pauillac.inria.fr/ ~boutin/publis.html, 1996.

   Google Scholar 

10. N.G. de Bruijn. Lambda Calculus Notation with Nameless Dummies: a Tool for Automatic Formula Manipulation, with Application to the CurchRosser Theorem. In Indagationes Mathematicae, volume 34, pages 381–392. 1972.

    Google Scholar 

11. E. Giménez. Un calcul de constructions infinies et son application à la vérification de systèmes communicants. PhD thesis, E.N.S. Lyon, 1996.

    Google Scholar 

12. D. Hirschkoff. Up to context proofs for the π-calculus in the Coq system. Technical Report 97–82, CERMICS, Noisy-le-Grand, January 1997.

    Google Scholar 

13. G. Huet. Residual theory in λ-calculus: A formal development. Technical Report 2009, INRIA, Rocquencourt — France, Août 1993.

    Google Scholar 

14. J. Mc Kinna and R. Pollack. Pure Type Systems Formalized. In Proceedings of TLCA'93, volume 664 of LNCS Springer Verlag, 1993.

    Google Scholar 

15. T. F. Melham. A mechanized theory of the π-calculus in HOL. Nordic Journal of Computing, 1(1):50–76, 1994.

    Google Scholar 

16. T. F. Melham and A. Gordon. Five Axioms of Alpha-Conversion. In Proceedings of TPHOL'96, volume 1125 of LNCS. Springer Verlag, 1996.

    Google Scholar 

17. R. Milner. The polyadic π-calculus: a tutorial. Technical Report ECSLFCS-91-180 LFCS, Dept. of Computer Science, Un. of Edinburgh, 1991.

    Google Scholar 

18. D. Miller. The π-calculus as a theory in linear logic: Preliminary results. In E. Lamma and P. Mello, editors, Proceedings of the Workshop on Extensions to Logic Programming, volume 660 of Lecture Notes in Computer Science, pages 242–265. Springer-Verlag, 1992.

    Google Scholar 

19. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Parts I and II. Information and Computation, 100:1–77, September 1992.

    Google Scholar 

20. M. Nesi. A formalisation of the CCS process algebra in higher order logic. Technical Report 278, Computer Laboratory, University of Cambridge, December 1992.

    Google Scholar 

21. U. Nestmann and B. C. Pierce. Decoding choice encodings. In Proceedings of CONCUR '96, number 1119, August 1996.

    Google Scholar 

22. B.C. Pierce. Programming in the Pi-Calculus (Tutorial Notes). Computer Laboratory, Cambridge-UK, November 1995.

    Google Scholar 

23. D. Sangiorgi. Lazy functions and mobile processes. Technical Report RR2515, INRIA — Sophia Antipolis, 1995.

    Google Scholar 

24. Davide Sangiorgi. On the bisimulation proof method. Revised version of Technical Report ECS-LFCS-94-299, University of Edinburgh, 1994. An extended abstract can be found in Proc. of MFCS'95, LNCS 969, 1995.

    Google Scholar 

25. A. Stoughton. Substitution revisited. Theoretical Computer Science, 59:317–325, 1988.

    Google Scholar 

26. B. Werner. Une théorie des constructions inductives. Thèse de doctorat, Université Paris 7, 1994.

    Google Scholar 

Download references