{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:34Z","timestamp":1761611254884,"version":"3.41.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100012950","name":"INRIA","doi-asserted-by":"crossref","award":["DP0880549"],"award-info":[{"award-number":["DP0880549"]}],"id":[{"id":"10.13039\/100012950","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2010,1]]},"abstract":"<jats:p>\n            We specify the operational semantics and bisimulation relations for the finite \u03c6-calculus within a logic that contains the \u2207 quantifier for encoding\n            <jats:italic>generic judgments<\/jats:italic>\n            and definitions for encoding fixed points. Since we restrict to the finite case, the ability of the logic to unfold fixed points allows this logic to be complete for both the inductive nature of operational semantics and the coinductive nature of bisimulation. The \u2207 quantifier helps with the delicate issues surrounding the scope of variables within \u03c6-calculus expressions and their executions (proofs). We illustrate several merits of the logical specifications permitted by this logic: they are natural and declarative; they contain no side-conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations arise from familar logic distinctions; the interplay between the three quantifiers (\u2200, \u2203, and \u2207) and their scopes can explain the differences between early and late bisimulation and between various modal operators based on bound input and output actions; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for one-step transitions, bisimulation, and satisfaction in modal logic. We also illustrate how one can encode the \u03c6-calculus with replications, in an extended logic with induction and co-induction.\n          <\/jats:p>","DOI":"10.1145\/1656242.1656248","type":"journal-article","created":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T20:14:58Z","timestamp":1263932098000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Proof search specifications of bisimulation and modal logics for the \u03c0-calculus"],"prefix":"10.1145","volume":"11","author":[{"given":"Alwen","family":"Tiu","sequence":"first","affiliation":[{"name":"The Australian National University, Canberra, Australia"}]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[{"name":"INRIA-Saclay &amp; LIX, \u00c9cole Polytechnique, Palaiseau Cedex, France"}]}],"member":"320","published-online":{"date-parts":[[2010,1,22]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_28"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"Baelde D.\n     and \n      Miller D\n  . \n  2007\n  . Least and greatest fixed points in linear logic. In International Conference on Logic for Programming and Automated Reasoning (LPAR) Lecture Notes in Artificial Intelligence vol. \n  4790\n  . \n  Springer-Verlag Berlin Germany 92--106.   Baelde D. and Miller D. 2007. Least and greatest fixed points in linear logic. In International Conference on Logic for Programming and Automated Reasoning (LPAR) Lecture Notes in Artificial Intelligence vol. 4790. Springer-Verlag Berlin Germany 92--106.","DOI":"10.1007\/978-3-540-75560-9_9"},{"key":"e_1_2_2_4_1","volume-title":"International Conference on Logic Programming (ICLP). Lecture Notes in Artificial Intelligence","volume":"2237","author":"Basu S.","unstructured":"Basu , S. , Mukund , M. , Ramakrishnan , C. R. , Ramakrishnan , I. V. , and Verma , R. M . 2001. Local and symbolic bisimulation using tabled constraint logic programming . In International Conference on Logic Programming (ICLP). Lecture Notes in Artificial Intelligence , vol. 2237 . Springer-Verlag, Berlin, Germany, 166--180. Basu, S., Mukund, M., Ramakrishnan, C. R., Ramakrishnan, I. V., and Verma, R. M. 2001. Local and symbolic bisimulation using tabled constraint logic programming. In International Conference on Logic Programming (ICLP). Lecture Notes in Artificial Intelligence, vol. 2237. Springer-Verlag, Berlin, Germany, 166--180."},{"key":"e_1_2_2_5_1","volume-title":"Proceedings of the International Conference on Foundations of Softwave Science and Computation Structures (FOSSACS","volume":"4423","author":"Bengtson J.","year":"2007","unstructured":"Bengtson , J. and Parrow , J . 2007. Formalising the &pi;-calculus using nominal logic . In Proceedings of the International Conference on Foundations of Softwave Science and Computation Structures (FOSSACS 2007 ). Lecture Notes in Computer Science , vol. 4423 . Springer-Verlag, Berlin, Germany, 63--77. Bengtson, J. and Parrow, J. 2007. Formalising the &pi;-calculus using nominal logic. In Proceedings of the International Conference on Foundations of Softwave Science and Computation Structures (FOSSACS 2007). Lecture Notes in Computer Science, vol. 4423. Springer-Verlag, Berlin, Germany, 63--77."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/646254.684259"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0032"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_2_2_10_1","volume-title":"Proceedings of the IFIP International Conference on Theoretical Computer Science (IFIP TCS'2000)","author":"Despeyroux J.","year":"2000","unstructured":"Despeyroux , J. 2000 . A higher-order specification of the &pi;-calculus . In Proceedings of the IFIP International Conference on Theoretical Computer Science (IFIP TCS'2000) . North-Holland, Amsterdam, The Netherlands, 425--439. Despeyroux, J. 2000. A higher-order specification of the &pi;-calculus. In Proceedings of the IFIP International Conference on Theoretical Computer Science (IFIP TCS'2000). North-Holland, Amsterdam, The Netherlands, 425--439."},{"key":"e_1_2_2_11_1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proceedings of the 2nd International Workshop on Extensions to Logic Programming","author":"Eriksson L.-H.","unstructured":"Eriksson , L.-H. 1991. A finitary version of the calculus of partial inductive definitions . In Proceedings of the 2nd International Workshop on Extensions to Logic Programming . Lecture Notes in Artificial Intelligence , vol. 596 . Springer-Verlag , Berlin, Germany , 89--134. Eriksson, L.-H. 1991. A finitary version of the calculus of partial inductive definitions. In Proceedings of the 2nd International Workshop on Extensions to Logic Programming. Lecture Notes in Artificial Intelligence, vol. 596. Springer-Verlag, Berlin, Germany, 89--134."},{"key":"e_1_2_2_12_1","unstructured":"Gabbay M. J. 2003. The &pi;-calculus in FM. In Thirty-five years of Automath F. Kamareddine Ed. Kluwer 80--149.  Gabbay M. J. 2003. The &pi;-calculus in FM. In Thirty-five years of Automath F. Kamareddine Ed. Kluwer 80--149."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"volume-title":"The Collected Papers of Gerhard Gentzen. North-Holland","author":"Gentzen G.","key":"e_1_2_2_14_1","unstructured":"Gentzen , G. 1969. Investigations into logical deductions . In The Collected Papers of Gerhard Gentzen. North-Holland , Amsterdam , 68--131. Gentzen, G. 1969. Investigations into logical deductions. In The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, 68--131."},{"key":"e_1_2_2_15_1","unstructured":"Girard J.-Y. 1992. A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu.  Girard J.-Y. 1992. A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.5.635"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00172-F"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/646524.756866"},{"volume-title":"Proceedings of the Workshop on Programming Concepts and Methods (PROCOMET'98)","author":"Honsell F.","key":"e_1_2_2_19_1","unstructured":"Honsell , F. , Lenisa , M. , Montanari , U. , and Pistore , M . 1998. Final semantics for the &pi;-calculus . In Proceedings of the Workshop on Programming Concepts and Methods (PROCOMET'98) . Springer-Verlag, Berlin, Germany. Honsell, F., Lenisa, M., Montanari, U., and Pistore, M. 1998. Final semantics for the &pi;-calculus. In Proceedings of the Workshop on Programming Concepts and Methods (PROCOMET'98). Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00095-5"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264598"},{"key":"e_1_2_2_23_1","volume-title":"CSL 2007: Proceedings of the Symposium on Computer Science Logic. Lecture Notes in Computer Science","volume":"4646","author":"Liang C.","unstructured":"Liang , C. and Miller , D . 2007. Focusing and polarization in intuitionistic logic . In CSL 2007: Proceedings of the Symposium on Computer Science Logic. Lecture Notes in Computer Science , vol. 4646 . Springer-Verlag, Berlin, Germany, 451--465. (Extended version to appear in TCS). Liang, C. and Miller, D. 2007. Focusing and polarization in intuitionistic logic. In CSL 2007: Proceedings of the Symposium on Computer Science Logic. Lecture Notes in Computer Science, vol. 4646. Springer-Verlag, Berlin, Germany, 451--465. (Extended version to appear in TCS)."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00171-1"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504080"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00168-2"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/647482.728283"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.3115\/981131.981165"},{"volume-title":"Proceedings of the IEEE Symposium on Logic Programming. IEEE Computer Society Press","author":"Miller D.","key":"e_1_2_2_31_1","unstructured":"Miller , D. and Nadathur , G . 1987. A logic programming approach to manipulating formulas and programs . In Proceedings of the IEEE Symposium on Logic Programming. IEEE Computer Society Press , Los Alamitos, CA, 379--388. Miller, D. and Nadathur, G. 1987. A logic programming approach to manipulating formulas and programs. In Proceedings of the IEEE Symposium on Logic Programming. IEEE Computer Society Press, Los Alamitos, CA, 379--388."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/333580.333590"},{"volume-title":"Proceedings of the 18th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Miller D.","key":"e_1_2_2_34_1","unstructured":"Miller , D. and Tiu , A . 2003. A proof theory for generic judgments: An extended abstract . In Proceedings of the 18th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press , Los Alamitos, CA, 118--127. Miller, D. and Tiu, A. 2003. A proof theory for generic judgments: An extended abstract. In Proceedings of the 18th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 118--127."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90009-5"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90156-N"},{"key":"e_1_2_2_38_1","volume-title":"Post-proceedings of TYPES","volume":"3058","author":"Momigliano A.","year":"2003","unstructured":"Momigliano , A. and Tiu , A . 2003. Induction and co-induction in sequent calculus . In Post-proceedings of TYPES 2003 . Lecture Notes in Computer Science , vol. 3058 . Springer-Verlag, Berlin, Germany, 293--308. Momigliano, A. and Tiu, A. 2003. Induction and co-induction in sequent calculus. In Post-proceedings of TYPES 2003. Lecture Notes in Computer Science, vol. 3058. Springer-Verlag, Berlin, Germany, 293--308."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002297"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562931_28"},{"volume-title":"Proceedings of the 5th International Logic Programming Conference. MIT Press","author":"Nadathur G.","key":"e_1_2_2_41_1","unstructured":"Nadathur , G. and Miller , D . 1988. An overview of \u03bb Prolog . In Proceedings of the 5th International Logic Programming Conference. MIT Press , Cambridge, MA, 810--827. Nadathur, G. and Miller, D. 1988. An overview of \u03bb Prolog. In Proceedings of the 5th International Logic Programming Conference. MIT Press, Cambridge, MA, 810--827."},{"key":"e_1_2_2_42_1","volume-title":"Proceedings of the 16th Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence","volume":"1652","author":"Nadathur G.","unstructured":"Nadathur , G. and Mitchell , D. J . 1999. System description: Teyjus\u2014A compiler and abstract machine based implementation of \u03bb Prolog . In Proceedings of the 16th Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence , vol. 1652 . Springer-Verlag, Berlin, Germany, 287--291. Nadathur, G. and Mitchell, D. J. 1999. System description: Teyjus\u2014A compiler and abstract machine based implementation of \u03bb Prolog. In Proceedings of the 16th Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 1652. Springer-Verlag, Berlin, Germany, 287--291."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287599"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(86)90015-4"},{"key":"e_1_2_2_45_1","volume-title":"Isabelle: The next 700 theorem provers. In Logic and Computer Science","author":"Paulson L. C.","year":"1990","unstructured":"Paulson , L. C. 1990 . Isabelle: The next 700 theorem provers. In Logic and Computer Science . Academic Press , Orlando, FL , 361--386. Paulson, L. C. 1990. Isabelle: The next 700 theorem provers. In Logic and Computer Science. Academic Press, Orlando, FL, 361--386."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_2_2_47_1","volume-title":"Proceedings of the 16th Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence","volume":"1632","author":"Pfenning F.","unstructured":"Pfenning , F. and Sch\u00fcrmann , C . 1999. System description: Twelf\u2014A meta-logical framework for deductive systems . In Proceedings of the 16th Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence , vol. 1632 . Springer-Verlag, Berlin, Germany, 202--206. Pfenning, F. and Sch\u00fcrmann, C. 1999. System description: Twelf\u2014A meta-logical framework for deductive systems. In Proceedings of the 16th Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 1632. Springer-Verlag, Berlin, Germany, 202--206."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"volume-title":"A structural approach to operational semantics. DAIMI FN-19","author":"Plotkin G.","key":"e_1_2_2_49_1","unstructured":"Plotkin , G. 1981. A structural approach to operational semantics. DAIMI FN-19 , Aarhus University , Aarhus, Denmark . Sept. Plotkin, G. 1981. A structural approach to operational semantics. DAIMI FN-19, Aarhus University, Aarhus, Denmark. Sept."},{"key":"e_1_2_2_50_1","unstructured":"Prawitz D. 1965. Natural Deduction. Almqvist & Wiksell Uppsala Sweden.  Prawitz D. 1965. Natural Deduction. Almqvist & Wiksell Uppsala Sweden."},{"key":"e_1_2_2_51_1","volume-title":"Proceedings of the International Conference on Foundations of Softwere Science and Computation Structures (FOSSACS'01)","volume":"2030","author":"R\u00f6ckl C.","unstructured":"R\u00f6ckl , C. , Hirschkoff , D. , and Berghofer , S . 2001. Higher-order abstract syntax with induction in Isabelle\/HOL: Formalizing the pi-calculus and mechanizing the theory of contexts . In Proceedings of the International Conference on Foundations of Softwere Science and Computation Structures (FOSSACS'01) . Lecture Notes in Computer Science , vol. 2030 . Springer-Verlag, Berlin, Germany, 364--378. R\u00f6ckl, C., Hirschkoff, D., and Berghofer, S. 2001. Higher-order abstract syntax with induction in Isabelle\/HOL: Formalizing the pi-calculus and mechanizing the theory of contexts. In Proceedings of the International Conference on Foundations of Softwere Science and Computation Structures (FOSSACS'01). Lecture Notes in Computer Science, vol. 2030. Springer-Verlag, Berlin, Germany, 364--378."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050036"},{"key":"e_1_2_2_53_1","unstructured":"Sangiorgi D. and Walker D. 2001. &pi;-Calculus: A Theory of Mobile Processes. Cambridge University Press Cambridge MA.   Sangiorgi D. and Walker D. 2001. &pi;-Calculus: A Theory of Mobile Processes. Cambridge University Press Cambridge MA."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287585"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054194000086"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_7"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.05.006"},{"volume-title":"Proceedings of the Symposium on Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL'05)","author":"Tiu A.","key":"e_1_2_2_59_1","unstructured":"Tiu , A. , Nadathur , G. , and Miller , D . 2005. Mixing finite success and finite failure in an automated prover . In Proceedings of the Symposium on Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL'05) . 79--98. Tiu, A., Nadathur, G., and Miller, D. 2005. Mixing finite success and finite failure in an automated prover. In Proceedings of the Symposium on Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL'05). 79--98."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_4"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.09.032"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1656242.1656248","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1656242.1656248","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:41:18Z","timestamp":1750250478000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1656242.1656248"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,1]]}},"alternative-id":["10.1145\/1656242.1656248"],"URL":"https:\/\/doi.org\/10.1145\/1656242.1656248","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2010,1]]},"assertion":[{"value":"2008-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}