{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:05:54Z","timestamp":1781172354737,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540425250","type":"print"},{"value":"9783540447559","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44755-5_16","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T06:03:32Z","timestamp":1186725812000},"page":"217-232","source":"Crossref","is-referenced-by-count":8,"title":["A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Simon J.","family":"Gay","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. deBruijn","year":"1972","unstructured":"N. G. deBruijn. Lambda calculus notation with nameless dummies. Indagationes Mathematicae, 34:381\u2013392, 1972.","journal-title":"Indagationes Mathematicae"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"J. Despeyroux. A higher-order specification of the pi-calculus. In Proceedings of the IFIP International Conference on Theoretical Computer Science, 2000.","DOI":"10.1007\/3-540-44929-9_30"},{"key":"16_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-44659-1_9","volume-title":"Proceedings of TPHOLs2000, the 13th International Conference on Theorem Proving in Higher Order Logics","author":"C. Dubois","year":"2000","unstructured":"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\u2013144. Springer, 2000."},{"key":"16_CR4","unstructured":"M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 2001."},{"key":"16_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49099-X_6","volume-title":"ESOP\u201999: Proceedings of the European Symposium on Programming Languages and Systems","author":"S. J. Gay","year":"1999","unstructured":"S. J. Gay and M. J. Hole. Types and subtypes for client-server interactions. In S. D. Swierstra, editor, ESOP\u201999: Proceedings of the European Symposium on Programming Languages and Systems, number 1576 in Lecture Notes in Computer Science, pages 74\u201390. Springer-Verlag, 1999."},{"issue":"1","key":"16_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50(1):1\u2013102, 1987.","journal-title":"Theoretical Computer Science"},{"key":"16_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BFb0105404","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996","author":"A. D. Gordon","year":"1996","unstructured":"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\u201996, volume 1125 of Lecture Notes in Computer Science, pages 173\u2013190. Springer-Verlag, 1996."},{"key":"16_CR8","unstructured":"L. Henry-Gr\u00e9ard. Proof of the subject reduction property for a \u03c0-calculus in COQ. Technical Report 3698, INRIA Sophia-Antipolis, May 1999."},{"key":"16_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0028392","volume-title":"Proceedings of the Tenth International Conference on Theorem Proving in Higher Order Logics","author":"D. Hirschkoff","year":"1997","unstructured":"D. Hirschkoff. A full formalisation of \u03c0-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\u2013169. Springer-Verlag, 1997."},{"key":"16_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the European Symposium on Programming","author":"Honda","year":"1998","unstructured":"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."},{"issue":"2","key":"16_CR11","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F. Honsell","year":"2001","unstructured":"F. Honsell, M. Miculan, and I. Scagnetto. \u03c0-calculus in (co)inductive type theory. Theoretical Computer Science, 253(2):239\u2013285, 2001.","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"16_CR12","doi-asserted-by":"crossref","first-page":"914","DOI":"10.1145\/330249.330251","volume":"21","author":"N. Kobayashi","year":"1999","unstructured":"N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the Pi-Calculus. ACM Transactions on Programming Languages and Systems, 21(5):914\u2013947, September 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"J. McKinna and R. Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23(3), 1999.","DOI":"10.1023\/A:1006294005493"},{"issue":"1","key":"16_CR14","first-page":"50","volume":"1","author":"T. F. Melham","year":"1994","unstructured":"T. F. Melham. A mechanized theory of the \u03c0-calculus in HOL. Nordic Journal of Computing, 1(1):50\u201376, 1994.","journal-title":"Nordic Journal of Computing"},{"key":"16_CR15","unstructured":"R. Milner. The polyadic \u03c0-calculus: A tutorial. Technical Report 91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1991."},{"key":"16_CR16","unstructured":"R. Milner. Communicating and Mobile Systems: the \u03c0-calculus. Cambridge University Press, 1999."},{"issue":"1","key":"16_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1\u201377, September 1992.","journal-title":"Information and Computation"},{"key":"16_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle \u2014 A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle \u2014 A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN\u2019 88 Symposium on Programming Language Design and Implementation. ACM Press, 1988.","DOI":"10.1145\/53990.54010"},{"key":"16_CR20","unstructured":"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."},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"C. R\u00f6ckl. A first-order syntax for the pi-calculus in Isabelle\/HOL using permutations. Technical report, D\u00e9partement d\u2019Informatique, \u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne, 2001.","DOI":"10.1016\/S1571-0661(04)00276-2"},{"key":"16_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-45315-6_24","volume-title":"Proceedings of FOSSACS\u201901","author":"C. R\u00f6ckl","year":"2001","unstructured":"C. R\u00f6ckl, 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\u201901, number 2030 in Lecture Notes in Computer Science, pages 364\u2013378. Springer-Verlag, 2001."},{"key":"16_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48737-9_3","volume-title":"Formal Syntax and Semantics of Java","author":"D. Syme","year":"1999","unstructured":"D. Syme. Proving Java type soundness. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of LNCS. Springer, 1999."},{"key":"16_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 6th European Conference on Parallel Languages and Architectures","author":"K. Takeuchi","year":"1994","unstructured":"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."},{"key":"16_CR25","unstructured":"D. N. Turner. The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, University of Edinburgh, 1996."},{"key":"16_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-48737-9_4","volume-title":"Formal Syntax and Semantics of Java","author":"D. Oheimb von","year":"1999","unstructured":"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\u2013156. Springer, 1999."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44755-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:10:41Z","timestamp":1556734241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425250","9783540447559"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-44755-5_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}