{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:38:11Z","timestamp":1725536291275},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_9","type":"book-chapter","created":{"date-parts":[[2009,8,20]],"date-time":"2009-08-20T01:46:12Z","timestamp":1250732772000},"page":"99-114","source":"Crossref","is-referenced-by-count":13,"title":["Psi-calculi in Isabelle"],"prefix":"10.1007","author":[{"given":"Jesper","family":"Bengtson","sequence":"first","affiliation":[]},{"given":"Joachim","family":"Parrow","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","first-page":"104","volume-title":"Proceedings of POPL 2001","author":"M. Abadi","year":"2001","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of POPL 2001, pp. 104\u2013115. ACM, New York (2001)"},{"key":"9_CR2","first-page":"3","volume-title":"POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"B. Aydemir","year":"2008","unstructured":"Aydemir, B., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 3\u201315. ACM, New York (2008)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-24849-1_3","volume-title":"Types for Proofs and Programs","author":"C. Ballarin","year":"2004","unstructured":"Ballarin, C.: Locales and locale expressions in isabelle\/isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 34\u201350. Springer, Heidelberg (2004)"},{"key":"9_CR4","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus \u2013 Its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus \u2013 Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol.\u00a0103. North-Holland, Amsterdam (1984)"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: Mobile processes, nominal data, and logic. Technical report, Uppsala University (2009); (submitted), http:\/\/user.it.uu.se\/~joachim\/psi.pdf","DOI":"10.1109\/LICS.2009.20"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-540-71389-0_6","volume-title":"Foundations of Software Science and Computational Structures","author":"J. Bengtson","year":"2007","unstructured":"Bengtson, J., Parrow, J.: Formalising the pi-calculus using nominal logic. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, pp. 63\u201377. Springer, Heidelberg (2007)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-71067-7_10","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2008","unstructured":"Berghofer, S., Urban, C.: Nominal Inversion Principles. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 71\u201385. Springer, Heidelberg (2008)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-540-78739-6_20","volume-title":"Programming Languages and Systems","author":"M.G. Buscemi","year":"2008","unstructured":"Buscemi, M.G., Montanari, U.: Open bisimulation for the concurrent constraint \u03c0-calculus. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 254\u2013268. Springer, Heidelberg (2008)"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies. a tool for automatic formula manipulation with application to the church-rosser theorem. Indagationes Mathematicae\u00a034, 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0028392","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Hirschkoff","year":"1997","unstructured":"Hirschkoff, D.: A full formalisation of \u03c0-calculus theory in the calculus of constructions. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 153\u2013169. Springer, Heidelberg (1997)"},{"issue":"2","key":"9_CR11","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F. Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: \u03c0-calculus in (co)inductive type theory. Theoretical Comput. Sci.\u00a0253(2), 239\u2013285 (2001)","journal-title":"Theoretical Comput. Sci."},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation\u00a0186, 165\u2013193 (2003)","journal-title":"Information and Computation"},{"issue":"2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1017\/S0956796802004653","volume":"13","author":"C. R\u00f6ckl","year":"2003","unstructured":"R\u00f6ckl, C., Hirschkoff, D.: A fully adequate shallow embedding of the \u03c0-calculus in Isabelle\/HOL with mechanized syntax analysis. J. Funct. Program.\u00a013(2), 415\u2013451 (2003)","journal-title":"J. Funct. Program."},{"issue":"4","key":"9_CR15","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C. Urban","year":"2008","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. Journal of Automated Reasoning\u00a040(4), 327\u2013356 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-73595-3_4","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Urban","year":"2007","unstructured":"Urban, C., Berghofer, S., Norrish, M.: Barendregt\u2019s variable convention in rule inductions. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 35\u201350. Springer, Heidelberg (2007)"}],"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\/978-3-642-03359-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T02:48:17Z","timestamp":1558493297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}