{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,2]],"date-time":"2024-03-02T08:19:51Z","timestamp":1709367591789},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2009,1,21]]},"DOI":"10.1145\/1480881.1480934","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T14:41:38Z","timestamp":1232462498000},"update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Verifying distributed systems"],"prefix":"10.1145","author":[{"given":"Thomas","family":"Ridge","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2009,1,21]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"IEEE standards association POSIX. Available online at http:\/\/standards.ieee.org\/regauth\/posix\/. IEEE standards association POSIX. Available online at http:\/\/standards.ieee.org\/regauth\/posix\/."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1080091.1080123"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111043"},{"key":"e_1_3_2_1_4_1","unstructured":"M.\n Compton\n .\n Stenning's protocol implemented in UDP and verified in Isabelle\n . In M. D. Atkinson and F. K. H. A. Dehne editors CATS volume \n 41\n of \n CRPIT pages \n 21\n --\n 30\n . \n Australian Computer Society 2005\n . M. Compton. Stenning's protocol implemented in UDP and verified in Isabelle. In M. D. Atkinson and F. K. H. A. Dehne editors CATS volume 41 of CRPIT pages 21--30. Australian Computer Society 2005."},{"key":"e_1_3_2_1_5_1","unstructured":"M. Felleisen and M. Flatt. Programming languages and lambda calculi. Available online at http:\/\/www.cs.utah.edu\/plt\/publications\/pllc.pdf. M. Felleisen and M. Flatt. Programming languages and lambda calculi. Available online at http:\/\/www.cs.utah.edu\/plt\/publications\/pllc.pdf."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2005.22"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010246"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/69624.357207"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30142-4_14"},{"key":"e_1_3_2_1_13_1","volume-title":"Distributed Algorithms. Morgan Kaufmann","author":"Lynch N. A.","year":"1996","unstructured":"N. A. Lynch . Distributed Algorithms. Morgan Kaufmann , 1996 . N. A. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/647852.737558"},{"key":"e_1_3_2_1_17_1","first-page":"89","volume-title":"Formal Methods Europe (FME 2002","volume":"2391","author":"Oheimb D. v.","year":"2002","unstructured":"D. v. Oheimb and T. Nipkow . Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited. In L.-H. Eriksson and P. Lindsay, editors , Formal Methods Europe (FME 2002 ), volume 2391 , pages 89 -- 105 , 2002 . D. v. Oheimb and T. Nipkow. Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited. In L.-H. Eriksson and P. Lindsay, editors, Formal Methods Europe (FME 2002), volume 2391, pages 89--105, 2002."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"S.\n Owens\n .\n A sound semantics for OCaml light\n . In S. Drossopoulou editor ESOP volume \n 4960\n of \n Lecture Notes in Computer Science pages \n 1\n --\n 15\n . \n Springer 2008\n . S. Owens. A sound semantics for OCaml light. In S. Drossopoulou editor ESOP volume 4960 of Lecture Notes in Computer Science pages 1--15. Springer 2008.","DOI":"10.1007\/978-3-540-78739-6_1"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/353677.353681"},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/3-540-45699-6_8","volume-title":"Applied Semantics, Advanced Lectures","author":"Pitts A. M.","year":"2002","unstructured":"A. M. Pitts . Operational semantics and program equivalence . In G. Barthe, P. Dybjer, and J. Saraiva, editors, Applied Semantics, Advanced Lectures , volume 2395 of Lecture Notes in Computer Science , Tutorial, pages 378 -- 412 . Springer-Verlag , 2002 . A. M. Pitts. Operational semantics and program equivalence. In G. Barthe, P. Dybjer, and J. Saraiva, editors, Applied Semantics, Advanced Lectures, volume 2395 of Lecture Notes in Computer Science, Tutorial, pages 378--412. Springer-Verlag, 2002."},{"key":"e_1_3_2_1_22_1","first-page":"227","volume-title":"Higher Order Operational Techniques in Semantics","author":"Pitts A. M.","year":"1998","unstructured":"A. M. Pitts and I. D. B. Stark . Operational reasoning for functions with local state . In A. D. Gordon and A. M. Pitts, editors, Higher Order Operational Techniques in Semantics , Publications of the Newton Institute, pages 227 -- 273 . Cambridge University Press , 1998 . A. M. Pitts and I. D. B. Stark. Operational reasoning for functions with local state. In A. D. Gordon and A. M. Pitts, editors, Higher Order Operational Techniques in Semantics, Publications of the Newton Institute, pages 227--273. Cambridge University Press, 1998."},{"key":"e_1_3_2_1_23_1","volume-title":"The origins of structural operational semantics. Journal of Logic and Algebraic Programming (JLAP), 60:3--15","author":"Plotkin G. D.","year":"2004","unstructured":"G. D. Plotkin . The origins of structural operational semantics. Journal of Logic and Algebraic Programming (JLAP), 60:3--15 , 2004 . G. D. Plotkin. The origins of structural operational semantics. Journal of Logic and Algebraic Programming (JLAP), 60:3--15, 2004."},{"key":"e_1_3_2_1_24_1","volume-title":"A structural approach to operational semantics. Journal of Logic and Algebraic Progamming (JLAP), 60:17--139","author":"Plotkin G. D.","year":"2004","unstructured":"G. D. Plotkin . A structural approach to operational semantics. Journal of Logic and Algebraic Progamming (JLAP), 60:17--139 , 2004 . G. D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Progamming (JLAP), 60:17--139, 2004."},{"key":"e_1_3_2_1_25_1","volume-title":"a logic for shared mutable data structures","author":"Reynolds J.","year":"2002","unstructured":"J. Reynolds . Separation logic : a logic for shared mutable data structures , 2002 . J. Reynolds. Separation logic: a logic for shared mutable data structures, 2002."},{"key":"e_1_3_2_1_26_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/978-3-540-74591-4_21","volume-title":"Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs","author":"Ridge T.","year":"2007","unstructured":"T. Ridge . Operational reasoning for concurrent Caml programs and weak memory models . In K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007 , Kaiserslautern, Germany, September 10-13, 2007, Proceedings, volume 4732 of Lecture Notes in Computer Science , pages 278 -- 293 . Springer , 2007. T. Ridge. Operational reasoning for concurrent Caml programs and weak memory models. In K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, volume 4732 of Lecture Notes in Computer Science, pages 278--293. Springer, 2007."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_21"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392200.2392220"},{"key":"e_1_3_2_1_29_1","volume-title":"Morgan Kaufmann","author":"Weikum G.","year":"2002","unstructured":"G. Weikum and G. Vossen . Transactional Information Systems . Morgan Kaufmann , 2002 . G. Weikum and G. Vossen. Transactional Information Systems. Morgan Kaufmann, 2002."}],"event":{"name":"POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Savannah GA USA","acronym":"POPL09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1480881.1480934","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T21:21:49Z","timestamp":1693862509000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1480881.1480934"}},"subtitle":["the operational approach"],"short-title":[],"issued":{"date-parts":[[2009,1,21]]},"references-count":27,"alternative-id":["10.1145\/1480881.1480934","10.1145\/1480881"],"URL":"http:\/\/dx.doi.org\/10.1145\/1480881.1480934","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1594834.1480934","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2009,1,21]]},"assertion":[{"value":"2009-01-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}