{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:12:33Z","timestamp":1725516753620},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705826"},{"type":"electronic","value":"9783540705833"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70583-3_9","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"99-111","source":"Crossref","is-referenced-by-count":9,"title":["Completeness and Logical Full Abstraction in Modal Logics for Typed Mobile Processes"],"prefix":"10.1007","author":[{"given":"Martin","family":"Berger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kohei","family":"Honda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Full version of this paper as a DoC technical report, Imperial College London (to appear, 2008) www.dcs.qmul.ac.uk\/~kohei\/processlogic"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-61648-9_50","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"R. Amadio","year":"1996","unstructured":"Amadio, R., Dam, M.: A modal theory of types for the \u03c0-calculus. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol.\u00a01135, pp. 347\u2013365. Springer, Heidelberg (1996)"},{"key":"9_CR3","unstructured":"Berger, M.: A program logic for sequential higher-order control (1): stateless case. Typescript, 36 pages (October 2007)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/3-540-45413-6_7","volume-title":"Typed Lambda Calculi and Applications","author":"M. Berger","year":"2001","unstructured":"Berger, M., Honda, K., Yoshida, N.: Sequentiality and the \u03c0-calculus. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, pp. 29\u201345. Springer, Heidelberg (2001)"},{"key":"9_CR5","first-page":"303","volume-title":"LICS 2007","author":"M. Bonsangue","year":"2007","unstructured":"Bonsangue, M., Kurz, A.: Pi-calculus in logical form. In: LICS 2007, pp. 303\u2013312. IEEE, Los Alamitos (2007)"},{"issue":"2","key":"9_CR6","first-page":"194","volume":"186","author":"L. Caires","year":"2003","unstructured":"Caires, L., Cardelli, L.: A spatial logic for concurrency. I& C\u00a0186(2), 194\u2013235 (2003)","journal-title":"I& C"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Cardelli, L., Gordon, A.D.: Anytime, anywhere: Modal logics for mobile ambients. In: POPL, pp. 365\u2013377 (2000)","DOI":"10.1145\/325694.325742"},{"key":"9_CR8","series-title":"Trends in Logic, Studia Logica Library","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/0-306-48088-3_4","volume-title":"Logic for Concurrency and Synchronisation","author":"M. Dam","year":"2003","unstructured":"Dam, M.: Proof systems for pi-calculus logics. In: Logic for Concurrency and Synchronisation. Trends in Logic, Studia Logica Library, pp. 145\u2013212. Kluwer, Dordrecht (2003)"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/1016850.1016874","volume-title":"ICFP 2004","author":"K. Honda","year":"2004","unstructured":"Honda, K.: From process logic to program logic. In: ICFP 2004, pp. 163\u2013174. ACM, New York (2004)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/11787006_31","volume-title":"Automata, Languages and Programming","author":"K. Honda","year":"2006","unstructured":"Honda, K., Berger, M., Yoshida, N.: Descriptive and relative completeness for logics for higher-order functions. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 360\u2013371. Springer, Heidelberg (2006)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/BFb0053567","volume-title":"Programming Languages and Systems","author":"K. Honda","year":"1998","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language Primitives and Type Disciplines for Structured Communication-based Programming. In: Hankin, C. (ed.) ESOP 1998 and ETAPS 1998. LNCS, vol.\u00a01381, pp. 22\u2013138. Springer, Heidelberg (1998)"},{"key":"9_CR12","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321\u2013332 (1983)"},{"issue":"2&3","key":"9_CR13","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theor. Comput. Sci.\u00a072(2&3), 265\u2013288 (1990)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR14","unstructured":"Longley, J., Plotkin, G.: Logical full abstraction and PCF. In: Tbilisi Symposium on Logic, Language and Information, CLSI (1998)"},{"issue":"4","key":"9_CR15","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D. Miller","year":"2005","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Transactions on Computational Logic\u00a06(4), 749\u2013783 (2005)","journal-title":"ACM Transactions on Computational Logic"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Milner, R.: The polyadic \u03c0-calculus: A tutorial. In: Proceedings of the International Summer School on Logic Algebra of Specification, Marktoberdorf (1992)","DOI":"10.1007\/978-3-642-58041-3_6"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I and II. Info.& Comp.\u00a0100(1) (1992)","DOI":"10.1016\/0890-5401(92)90009-5"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0304-3975(93)90156-N","volume":"114","author":"R. Milner","year":"1993","unstructured":"Milner, R., Parrow, J., Walker, D.: Modal logics for mobile processes. TCS\u00a0114, 149\u2013171 (1993)","journal-title":"TCS"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/j.jlap.2004.03.004","volume":"60-61","author":"A. Simpson","year":"2004","unstructured":"Simpson, A.: Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS. J. Log. Algebr. Program.\u00a060-61, 287\u2013322 (2004)","journal-title":"J. Log. Algebr. Program."},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/BFb0015773","volume-title":"Automata, Languages and Programming","author":"C. Stirling","year":"1985","unstructured":"Stirling, C.: A complete compositional model proof system for a subset of CCS. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol.\u00a0194, pp. 475\u2013486. Springer, Heidelberg (1985)"},{"key":"9_CR21","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","volume":"49","author":"C. Stirling","year":"1987","unstructured":"Stirling, C.: Modal logics for communicating systems. TCS\u00a049, 311\u2013347 (1987)","journal-title":"TCS"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/3-540-58184-7_118","volume-title":"PARLE \u201994 Parallel Architectures and Languages Europe","author":"K. Takeuchi","year":"1994","unstructured":"Takeuchi, K., Honda, K., Kubo, M.: An Interaction-based Language and its Typing System. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol.\u00a0817, pp. 398\u2013413. Springer, Heidelberg (1994)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11539452_7","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A.F. Tiu","year":"2005","unstructured":"Tiu, A.F.: Model checking for pi-calculus using proof search. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 36\u201350. Springer, Heidelberg (2005)"},{"key":"9_CR24","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/j.ic.2003.08.004","volume":"191","author":"N. Yoshida","year":"2004","unstructured":"Yoshida, N., Berger, M., Honda, K.: Strong Normalisation in the \u03c0-Calculus. Information and Computation\u00a0191, 145\u2013202 (2004)","journal-title":"Information and Computation"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-540-71389-0_26","volume-title":"Foundations of Software Science and Computational Structures","author":"N. Yoshida","year":"2007","unstructured":"Yoshida, N., Honda, K., Berger, M.: Logical reasoning for higher-order functions with local state. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, pp. 361\u2013377. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70583-3_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:08:07Z","timestamp":1605744487000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70583-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705826","9783540705833"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70583-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}