{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,8]],"date-time":"2025-06-08T22:27:04Z","timestamp":1749421624039},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678236"},{"type":"electronic","value":"9783540449294"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44929-9_30","type":"book-chapter","created":{"date-parts":[[2007,5,5]],"date-time":"2007-05-05T13:20:53Z","timestamp":1178371253000},"page":"425-439","source":"Crossref","is-referenced-by-count":11,"title":["A Higher-Order Specification of the \u03c0-Calculus"],"prefix":"10.1007","author":[{"given":"Jo\u00eblle","family":"Despeyroux","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"30_CR1","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin, A. Sa\u00efbi, and B. Werner. The Coq Proof Assistant Reference Manual \u2014 Version V6.1. Technical Report 0203, INRIA, August 1997."},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"G\u00e9rard Boudol. The pi-calculus in direct style. In proceedings of the POPL ACM Conference on Principles of Programming Languages, pages 228\u2013241, 1997.","DOI":"10.1145\/263699.263726"},{"key":"30_CR3","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Thierry Coquand and G\u00e9rard Huet. The calculus of constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"30_CR4","series-title":"Lect Notes Comput Sci","volume-title":"proceedings of the annual Types for Proofs and Programs seminar","author":"J. Despeyroux","year":"1998","unstructured":"Jo\u00eblle Despeyroux and Pierre Leleu. A modal \u03bb-calcul with iteration and case constructs. In proceedings of the annual Types for Proofs and Programs seminar, Springer-Verlag LNCS 1657, March 1998. An extended and revised version will appear in the forthcoming special issue of MSCS on Intuitionistic Modal Logics and Applications."},{"key":"30_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-62688-3_34","volume-title":"proceedings of the TLCA 97 Int. Conference on Typed Lambda Calculi and Applications, Nancy, France, April 2\u20134","author":"J. Despeyroux","year":"1997","unstructured":"Jo\u00eblle Despeyroux, Frank Pfenning, and Carsten Sch\u00fcrmann. Primitive recursion for higher-order abstract syntax. In Philippe de Groote and J. Roger Hindley, editors, proceedings of the TLCA 97 Int. Conference on Typed Lambda Calculi and Applications, Nancy, France, April 2\u20134, pages 147\u2013163. Springer-Verlag LNCS 1210, April 1997. An extended version is available as CMU Technical Report CMU-CS-96-172. An extended and revised version will appear in TCS (Theoretical Computer Science)."},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"C\u00e9dric Fournet, Georges Gonthier, Jean-Jacques L\u00e9vy, Luc Maranget, and Didier R\u00e9my. A calculus of mobile agents. In Proc. of the CONCUR conference, 1996.","DOI":"10.1007\/3-540-61604-7_67"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"A. Gordon and P. Hankin. A concurrent object calculus: reduction and typing. In proceedings of the HLCL Conference, 1998.","DOI":"10.1016\/S1571-0661(04)00145-8"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Guillaume Gillard. A formalization of a concurrent object calculus up to alpha-conversion. In Proceedings of the 17th International Conference on Automated Deduction, CADE-17, June 2000.","DOI":"10.1007\/10721959_33"},{"key":"30_CR9","series-title":"Lect Notes Comput Sci","first-page":"414","volume-title":"proceedings of the int. workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver","author":"A. Gordon","year":"1994","unstructured":"A. Gordon. A mechanisation of name-carrying syntax up to alpha-conversion. In proceedings of the int. workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver, Springer-Verlag LNCS 780, pages 414\u2013426, 1994."},{"key":"30_CR10","unstructured":"Lo\u00efc Henry Greard. A proof of type preservation for the pi-calculus in Coq. Research Report RR-3698, Inria, December 1998. Also available in the Coq Contrib library."},{"key":"30_CR11","volume-title":"proceedings of the International Conference on Theorem Proving in Higher Order Logics","author":"D. Hirschkoff","year":"1997","unstructured":"Daniel Hirschkoff. A full formalization of pi-calculus theory in the Calculus of Constructions. In Elsa Gunter, editor, proceedings of the International Conference on Theorem Proving in Higher Order Logics, Murray Hill, New Jersey, August 1997."},{"key":"30_CR12","unstructured":"Daniel Hirschkoff. Mise en oeuvre de preuves de bisimulation. Phd thesis, \u00c9cole Nationale des Ponts et Chauss\u00e9es (ENPC), January 1999. In French."},{"key":"30_CR13","volume-title":"Technical Report RT 0204","author":"G. Huet","year":"1997","unstructured":"G\u00e9rard Huet, Gilles Kahn, and Christine Paulin-Mohring. The coq proof assistant: a tutorial, version 6.1. Technical Report RT 0204, Inria, Rocquencourt, France, August 1997. page html: http:\/\/www.inria.fr\/RRRT\/RT-0204.html ."},{"key":"30_CR14","unstructured":"Furio Honsell, Marino Miculan, and Ivan Scagnetto. Pi-calculus in (co)Inductive Type Theory. to appear in TCS, 1999."},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. Semantical analysis of higher-order abstract syntax. In IEEE, editor, proceedings of the International Conference on Logic In Computer Sciences, LICS, 1999.","DOI":"10.1109\/LICS.1999.782616"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Naoki Kobayashi. A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems, 20\u20132, December 1998. A preliminary summary appeared in LICS\u201997.","DOI":"10.1145\/276393.278524"},{"key":"30_CR17","unstructured":"Robin Milner. The polyadic pi-calculus: a tutorial. Technical Report ECS-LFCS-91-180, LFCS, Edinburgh University, October 1991."},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax: An extended abstract. In Glynn Winskel, editor, Proceedings of the Twelfth Annual Symposium on Logic in Computer Science, Warsaw, Poland, June 1997. To appear.","DOI":"10.1109\/LICS.1997.614968"},{"key":"30_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"R. Milner, R. Parrow, and J. Walker. A calculus of mobile processes, (part I and II). Information and Computation, 100:1\u201377, 1992.","journal-title":"Information and Computation"},{"key":"30_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA\u201993","author":"C. Paulin-Mohring","year":"1992","unstructured":"Christine Paulin-Mohring. Inductive definitions in the system coq. rules and properties. In J.F. Groote M. Bezem, editor, Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA\u201993, Springer-Verlag LNCS 664, pages 328\u2013345, 1992. also available as a Research Report RR-92-49, Dec. 1992, ENS Lyon, France."},{"key":"30_CR21","unstructured":"Benjamin Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 11, 1995."},{"key":"30_CR22","unstructured":"Benjamin Pierce and David Turner. Pict: A programming language based on the pi-calculus. Technical Report., IU, 1997."}],"container-title":["Lecture Notes in Computer Science","Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44929-9_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T18:40:50Z","timestamp":1556390450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44929-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678236","9783540449294"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44929-9_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}