{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T21:22:37Z","timestamp":1784150557869,"version":"3.55.0"},"reference-count":37,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2001,2,1]],"date-time":"2001-02-01T00:00:00Z","timestamp":980985600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4549,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2001,2]]},"DOI":"10.1016\/s0304-3975(00)00095-5","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T21:01:59Z","timestamp":1027630919000},"page":"239-285","source":"Crossref","is-referenced-by-count":72,"title":["\u03c0-calculus in (Co)inductive-type theory"],"prefix":"10.1016","volume":"253","author":[{"given":"Furio","family":"Honsell","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marino","family":"Miculan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ivan","family":"Scagnetto","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00095-5_BIB1","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00245294","article-title":"Using typed lambda calculus to implement formal systems on a machine","volume":"9","author":"Avron","year":"1992","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB2","unstructured":"The Coq Proof Assistant Reference Manual \u2013 Version 6.2, INRIA, May 1998, Available at ftp:\/\/ftp.inria.fr\/INRIA\/coq\/V6.2\/doc."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB3","first-page":"62","article-title":"Infinite objects in type theory","volume":"vol. 806","author":"Coquand","year":"1994"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB4","first-page":"95","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Inform. and Control"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB5","first-page":"85","article-title":"Automating inversion and inductive predicates in Coq","volume":"vol. 1158","author":"Cornes","year":"1996"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB6","doi-asserted-by":"crossref","unstructured":"J. Despeyroux, A. Felty, A. Hirschowitz, Higher-order syntax in Coq, Proc. TLCA\u201995, Lecture Notes in Computer Science, vol. 905, Springer, Berlin, 1995.","DOI":"10.1007\/BFb0014049"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB7","doi-asserted-by":"crossref","unstructured":"J. Despeyroux, F. Pfenning, C. Sch\u00fcrmann, Primitive recursion for higher order abstract syntax, CMU-CS-96-172, School of Computer Science, Carnegie Mellon University, Pittsburgh, August 1996.","DOI":"10.1007\/3-540-62688-3_34"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB8","unstructured":"M. Felchero, Sistemi di transizione in teoria dei tipi coinduttivi, Laurea's Thesis, Universit\u00e0 di Udine, Italy, July 1996 (in Italian)."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB9","unstructured":"H. Geuvers, Inductive and coinductive types with iteration and recursion. Available at http:\/\/www.dcs.ed.ac.uk\/lfcsinfo\/research\/ types_bra\/proc\/proc92.dvi.gz, June 1992."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB10","series-title":"Codifying guarded recursion definitions with recursive schemes, Proc. TYPES\u201994, Lecture Notes in Computer Science, vol. 996","author":"Gim\u00e9nez","year":"1995"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB11","first-page":"134","article-title":"An application of co-inductive types in Coq","volume":"vol. 1158","author":"Gim\u00e9nez","year":"1996"},{"issue":"1","key":"10.1016\/S0304-3975(00)00095-5_BIB12","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB13","series-title":"Bisimulation proofs for the \u03c0-calculus in the Calculus of Constructions, Proc. TPHOL\u201997, Lecture Notes in Computer Science, vol. 1275","author":"Hirschkoff","year":"1997"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB14","series-title":"Final semantics for the \u03c0-calculus, Proc. PROCOMET\u201998","author":"Honsell","year":"1998"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB15","first-page":"165","article-title":"A natural deduction approach to dynamic logics","volume":"vol. 1158","author":"Honsell","year":"1996"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB16","doi-asserted-by":"crossref","unstructured":"M. Hofmann, Semantical analysis of higher-order abstract syntax, Proc. 14th LICS, IEEE, New York, 1999.","DOI":"10.1109\/LICS.1999.782616"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB17","unstructured":"M. Lenisa, Themes in final semantics, Ph.D. Thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Italy, March 1998."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB18","unstructured":"P. Martin-L\u00f6f, On the meaning of the logical constants and the justifications of the logic laws, TR 2, Dip. di Matematica, Universit\u00e0 di Siena, 1985."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB19","doi-asserted-by":"crossref","unstructured":"R. McDowell, D. Miller, A logic for reasoning with higher-order abstract syntax, Proc. 12th LICS, IEEE, New York, 1997.","DOI":"10.1109\/LICS.1997.614968"},{"issue":"1","key":"10.1016\/S0304-3975(00)00095-5_BIB20","first-page":"50","article-title":"A mechanized theory of the \u03c0-calculus in HOL","volume":"1","author":"Melham","year":"1994","journal-title":"Nordic J. Comput."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB21","doi-asserted-by":"crossref","unstructured":"M. Miculan, The expressive power of structural operational semantics with explicit assumptions, in: Proc. TYPES\u201993 Lecture Notes in Computer Science, vol. 806, Springer, Berlin, 1994, pp. 292\u2013320.","DOI":"10.1007\/3-540-58085-9_80"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB22","unstructured":"M. Miculan, Encoding logical theories of programs, Ph.D. Thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Italy, March 1997."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB23","doi-asserted-by":"crossref","unstructured":"R. Milner, The polyadic \u03c0-calculus: a tutorial, in: Logic and Algebra of Specification, NATO ASI Series F, vol. 94, Springer, Berlin, 1993.","DOI":"10.1007\/978-3-642-58041-3_6"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB24","unstructured":"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."},{"issue":"1","key":"10.1016\/S0304-3975(00)00095-5_BIB25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes","volume":"100","author":"Milner","year":"1992","journal-title":"Inform. and Comput."},{"issue":"1","key":"10.1016\/S0304-3975(00)00095-5_BIB26","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/0304-3975(93)90156-N","article-title":"Modal logics for mobile processes","volume":"114","author":"Milner","year":"1993","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB27","doi-asserted-by":"crossref","unstructured":"T. Nipkow, L.C. Paulson, Isabelle-91 \u2013 System abstract, Proc. CADE 11, Lecture Notes in Computer Science, vol. 607, Springer, Berlin, 1992, pp. 673\u2013676.","DOI":"10.1007\/3-540-55602-8_201"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB28","series-title":"Programming in Martin-L\u00f6f's Type Theory: An Introduction","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB29","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring, Inductive definitions in the system Coq; rules and properties, Proc. TLCA\u201994, Lecture Notes in Computer Science, vol. 664, Springer, Berlin, 1993, pp. 328\u2013345.","DOI":"10.1007\/BFb0037116"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB30","doi-asserted-by":"crossref","unstructured":"F. Pfenning, C. Elliott, Higher-order abstract syntax, Proc. ACM SIGPLAN \u201988, ACM, New York, June 1988, pp. 199\u2013208.","DOI":"10.1145\/53990.54010"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB31","unstructured":"R. Pollack, The theory of LEGO, Ph.D. Thesis, Univ. of Edinburgh, 1994."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB32","unstructured":"A. Rossi, Tipi di dati coinduttivi: i reali, Laurea's Thesis, Universit\u00e0 di Udine, Italy, 1994."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB33","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s002360050036","article-title":"A theory of bisimulation for the \u03c0-calculus","volume":"33","author":"Sangiorgi","year":"1996","journal-title":"Acta Inform."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB34","unstructured":"I. Scagnetto, Rappresentazione di algebre di processi in logical frameworks, Laurea's Thesis, Universit\u00e0 di Udine, March 1997 (in italian)."},{"issue":"4","key":"10.1016\/S0304-3975(00)00095-5_BIB35","doi-asserted-by":"crossref","first-page":"1284","DOI":"10.2307\/2274279","article-title":"A natural extension of natural deduction","volume":"49","author":"Schroeder-Heister","year":"1984","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(00)00095-5_BIB36","unstructured":"Proc. TYPES\u201993, Lecture Notes in Computer Science, vol. 806, Springer, Berlin, 1994."},{"key":"10.1016\/S0304-3975(00)00095-5_BIB37","unstructured":"Proc. TYPES\u201995, Lecture Notes in Computer Science, vol. 1158, Springer, Berlin, 1996."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500000955?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500000955?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,4,13]],"date-time":"2023-04-13T14:28:22Z","timestamp":1681396102000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500000955"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,2]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,2]]}},"alternative-id":["S0304397500000955"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00095-5","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2001,2]]}}}