A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL

1. N. G. deBruijn. Lambda calculus notation with nameless dummies. Indagationes Mathematicae, 34:381–392, 1972.

   MathSciNet  Google Scholar 

2. J. Despeyroux. A higher-order specification of the pi-calculus. In Proceedings of the IFIP International Conference on Theoretical Computer Science, 2000.

   Google Scholar 

3. C. Dubois. Proving ML type soundness within Coq. In M. Aagaard and J. Harrison, editors, Proceedings of TPHOLs2000, the 13th International Conference on Theorem Proving in Higher Order Logics, LNCS, pages 126–144. Springer, 2000.

   Chapter  Google Scholar 

4. M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 2001.

   Google Scholar 

5. S. J. Gay and M. J. Hole. Types and subtypes for client-server interactions. In S. D. Swierstra, editor, ESOP’99: Proceedings of the European Symposium on Programming Languages and Systems, number 1576 in Lecture Notes in Computer Science, pages 74–90. Springer-Verlag, 1999.

   Chapter  Google Scholar 

6. J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50(1):1–102, 1987.

   Article  MATH  MathSciNet  Google Scholar 

7. A. D. Gordon and T. Melham. Five axioms of alpha conversion. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96, volume 1125 of Lecture Notes in Computer Science, pages 173–190. Springer-Verlag, 1996.

   Google Scholar 

8. L. Henry-Gréard. Proof of the subject reduction property for a π-calculus in COQ. Technical Report 3698, INRIA Sophia-Antipolis, May 1999.

   Google Scholar 

9. D. Hirschkoff. A full formalisation of π-calculus theory in the calculus of constructions. In Proceedings of the Tenth International Conference on Theorem Proving in Higher Order Logics, volume 1275 of Lecture Notes in Computer Science, pages 153–169. Springer-Verlag, 1997.

   Chapter  Google Scholar 

10. Honda, V. Vasconcelos, and M. Kubo. Language primitives and type discipline for structured communication-based programming. In Proceedings of the European Symposium on Programming, Lecture Notes in Computer Science. Springer-Verlag, 1998.

    Google Scholar 

11. F. Honsell, M. Miculan, and I. Scagnetto. π-calculus in (co)inductive type theory. Theoretical Computer Science, 253(2):239–285, 2001.

    Article  MATH  MathSciNet  Google Scholar 

12. N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the Pi-Calculus. ACM Transactions on Programming Languages and Systems, 21(5):914–947, September 1999.

    Google Scholar 

13. J. McKinna and R. Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23(3), 1999.

    Google Scholar 

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

    MathSciNet  Google Scholar 

15. R. Milner. The polyadic π-calculus: A tutorial. Technical Report 91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1991.

    Google Scholar 

16. R. Milner. Communicating and Mobile Systems: the π-calculus. Cambridge University Press, 1999.

    Google Scholar 

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

    Google Scholar 

18. L. C. Paulson. Isabelle — A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

    MATH  Google Scholar 

19. F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN’ 88 Symposium on Programming Language Design and Implementation. ACM Press, 1988.

    Google Scholar 

20. Pierce and D. Sangiorgi. Types and subtypes for mobile processes. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1993.

    Google Scholar 

21. C. Röckl. A first-order syntax for the pi-calculus in Isabelle/HOL using permutations. Technical report, Département d’Informatique, École Polytechnique Fédérale de Lausanne, 2001.

    Google Scholar 

22. C. Röckl, D. Hirschkoff, and S. Berghofer. Higher-order abstract syntax with induction in Isabelle/HOL: Formalizing the pi-calculus and mechanizing the theory of contexts. In F. Honsell and M. Miculan, editors, Proceedings of FOSSACS’01, number 2030 in Lecture Notes in Computer Science, pages 364–378. Springer-Verlag, 2001.

    Google Scholar 

23. D. Syme. Proving Java type soundness. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of LNCS. Springer, 1999.

    Chapter  Google Scholar 

24. K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and its typing system. In Proceedings of the 6th European Conference on Parallel Languages and Architectures, number 817 in Lecture Notes in Computer Science. Springer-Verlag, 1994.

    Google Scholar 

25. D. N. Turner. The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, University of Edinburgh, 1996.

    Google Scholar 

26. D. von Oheimb and T. Nipkow. Machine-checking the Java specification: Proving type-safety. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of LNCS, pages 119–156. Springer, 1999.

    Chapter  Google Scholar 

Download references