{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:31:05Z","timestamp":1767929465578,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":79,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T00:00:00Z","timestamp":1515369600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,1,8]]},"DOI":"10.1145\/3167090","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"130-145","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["A monadic framework for relational verification: applied to information security, program equivalence, and optimizations"],"prefix":"10.1145","author":[{"given":"Niklas","family":"Grimm","sequence":"first","affiliation":[{"name":"Vienna University of Technology, Austria"}]},{"given":"Kenji","family":"Maillard","sequence":"additional","affiliation":[{"name":"Inria, France \/ ENS Paris, France"}]},{"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"Matteo","family":"Maffei","sequence":"additional","affiliation":[{"name":"Vienna University of Technology, Austria"}]},{"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Tahina","family":"Ramananandro","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, India"}]},{"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Santiago","family":"Zanella-B\u00e9guelin","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}]}],"member":"320","published-online":{"date-parts":[[2018,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"A Relational Logic for Higher-Order Programs. CoRR abs\/1703.05042","author":"Aguirre Alejandro","year":"2017","unstructured":"Alejandro Aguirre , Gilles Barthe , Marco Gaboardi , Deepak Garg , and Pierre-Yves Strub . 2017. A Relational Logic for Higher-Order Programs. CoRR abs\/1703.05042 ( 2017 ). http:\/\/arxiv.org\/abs\/1703.05042. Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub. 2017. A Relational Logic for Higher-Order Programs. CoRR abs\/1703.05042 (2017). http:\/\/arxiv.org\/abs\/1703.05042."},{"key":"e_1_3_2_1_2_1","volume-title":"Talk at 1st International Workshop on Hammers for Type Theories (HaTT)","author":"Aguirre Alejandro","unstructured":"Alejandro Aguirre , Catalin Hritcu , Chantal Keller , and Nikhil Swamy . 2016. From F* to SMT (extended abstract). Talk at 1st International Workshop on Hammers for Type Theories (HaTT) . Alejandro Aguirre, Catalin Hritcu, Chantal Keller, and Nikhil Swamy. 2016. From F* to SMT (extended abstract). Talk at 1st International Workshop on Hammers for Type Theories (HaTT)."},{"key":"e_1_3_2_1_3_1","volume-title":"Dijkstra Monads for Free. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, 515-529","author":"Ahman Danel","year":"2017","unstructured":"Danel Ahman , Catalin Hritcu , Kenji Maillard , Guido Mart\u00ednez , Gordon Plotkin , Jonathan Protzenko , Aseem Rastogi , and Nikhil Swamy . 2017 . Dijkstra Monads for Free. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, 515-529 . Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Mart\u00ednez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. 2017. Dijkstra Monads for Free. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, 515-529."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480925"},{"key":"e_1_3_2_1_5_1","first-page":"100","volume-title":"11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings (Lecture Notes in Computer Science), Roberto Giacobazzi (Ed.)","volume":"3148","author":"Amtoft Torben","year":"2004","unstructured":"Torben Amtoft and Anindya Banerjee . 2004 . Information Flow Analysis in Logical Form. In Static Analysis , 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings (Lecture Notes in Computer Science), Roberto Giacobazzi (Ed.) , Vol. 3148 . Springer , 100 - 115 . Torben Amtoft and Anindya Banerjee. 2004. Information Flow Analysis in Logical Form. In Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings (Lecture Notes in Computer Science), Roberto Giacobazzi (Ed.), Vol. 3148. Springer, 100-115."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_20"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062378"},{"key":"e_1_3_2_1_8_1","volume-title":"Verifying relational properties of functional programs by first-order refinement. Science of Computer Programming (March","author":"Asada Kazuyuki","year":"2016","unstructured":"Kazuyuki Asada , Ryosuke Sato , and Naoki Kobayashi . 2016. Verifying relational properties of functional programs by first-order refinement. Science of Computer Programming (March 2016 ). Kazuyuki Asada, Ryosuke Sato, and Naoki Kobayashi. 2016. Verifying relational properties of functional programs by first-order refinement. Science of Computer Programming (March 2016)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_3_2_1_10_1","volume-title":"Relational Logic with Framing and Hypotheses. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016","volume":"65","author":"Banerjee Anindya","year":"2016","unstructured":"Anindya Banerjee , David A. Naumann , and Mohammad Nikouei . 2016 . Relational Logic with Framing and Hypotheses. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016 , December 13-15, 2016, Chennai, India (LIPIcs), Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen (Eds.) , Vol. 65 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 11:1-11:16. Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. 2016. Relational Logic with Framing and Hypotheses. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India (LIPIcs), Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen (Eds.), Vol. 65. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 11:1-11:16."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.05.004"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_3_2_1_13_1","volume-title":"Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures (Lecture Notes in Computer Science)","author":"Barthe Gilles","unstructured":"Gilles Barthe , Fran\u00e7ois Dupressoir , Benjamin Gr\u00e9goire , C\u00e9sar Kunz , Benedikt Schmidt , and Pierre-Yves Strub . 2013a. EasyCrypt: A Tutorial . In Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures (Lecture Notes in Computer Science) , Alessandro Aldini, Javier Lopez, and Fabio Martinelli (Eds.), Vol. 8604 . Springer , 146-166. Gilles Barthe, Fran\u00e7ois Dupressoir, Benjamin Gr\u00e9goire, C\u00e9sar Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013a. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures (Lecture Notes in Computer Science), Alessandro Aldini, Javier Lopez, and Fabio Martinelli (Eds.), Vol. 8604. Springer, 146-166."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535847"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480894"},{"key":"e_1_3_2_1_17_1","first-page":"1","volume-title":"Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In 11th International Conference on Mathematics of Program Construction (Lecture Notes in Computer Science)","volume":"7342","author":"Barthe Gilles","year":"2012","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , and Santiago Zanella-B\u00e9guelin . 2012 . Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In 11th International Conference on Mathematics of Program Construction (Lecture Notes in Computer Science) , Vol. 7342 . Springer , 1 - 6 . http:\/\/hal.inria.fr\/docs\/00\/76\/58\/64\/PDF\/main.pdf. Gilles Barthe, Benjamin Gr\u00e9goire, and Santiago Zanella-B\u00e9guelin. 2012. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In 11th International Conference on Mathematics of Program Construction (Lecture Notes in Computer Science), Vol. 7342. Springer, 1-6. http:\/\/hal.inria.fr\/docs\/00\/76\/58\/64\/PDF\/main.pdf."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_3_2_1_19_1","first-page":"87","volume-title":"ITP 2016, Nancy, France, August 22-25, 2016, Proceedings (Lecture Notes in Computer Science), Jasmin Christian Blanchette and Stephan Merz (Eds.)","volume":"9807","author":"Bauerei\u00df Thomas","year":"2016","unstructured":"Thomas Bauerei\u00df , Armando Pesenti Gritti , Andrei Popescu , and Franco Raimondi . 2016 . CoSMed: A Confidentiality-Verified Social Media Platform. In Interactive Theorem Proving - 7th International Conference , ITP 2016, Nancy, France, August 22-25, 2016, Proceedings (Lecture Notes in Computer Science), Jasmin Christian Blanchette and Stephan Merz (Eds.) , Vol. 9807 . Springer , 87 - 106 . Thomas Bauerei\u00df, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. 2016. CoSMed: A Confidentiality-Verified Social Media Platform. In Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings (Lecture Notes in Computer Science), Jasmin Christian Blanchette and Stephan Merz (Eds.), Vol. 9807. Springer, 87-106."},{"key":"e_1_3_2_1_20_1","first-page":"729","volume-title":"CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees. In 2017 IEEE Symposium on Security and Privacy, SP 2017","author":"Bauerei\u00df Thomas","year":"2017","unstructured":"Thomas Bauerei\u00df , Armando Pesenti Gritti , Andrei Popescu , and Franco Raimondi . 2017 . CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees. In 2017 IEEE Symposium on Security and Privacy, SP 2017 , San Jose, CA, USA , May 22-26, 2017. IEEE Computer Society, 729 - 748 . Thomas Bauerei\u00df, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. 2017. CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees. In 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017. IEEE Computer Society, 729-748."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786536.2786544"},{"key":"e_1_3_2_1_22_1","first-page":"409","article-title":"The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs","volume":"2006","author":"Bellare Mihir","year":"2006","unstructured":"Mihir Bellare and Phillip Rogaway . 2006 . The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs . In Advances in Cryptology - EUROCRYPT 2006. 409 - 426 . Mihir Bellare and Phillip Rogaway. 2006. The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. In Advances in Cryptology - EUROCRYPT 2006. 409-426.","journal-title":"Advances in Cryptology - EUROCRYPT"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_1_24_1","first-page":"48","volume-title":"Proof-Relevant Logical Relations for Name Generation. In 11th International Conference on Typed Lambda Calculi and Applications (Lecture Notes in Computer Science)","volume":"7941","author":"Benton Nick","year":"2013","unstructured":"Nick Benton , Martin Hofmann , and Vivek Nigam . 2013 . Proof-Relevant Logical Relations for Name Generation. In 11th International Conference on Typed Lambda Calculi and Applications (Lecture Notes in Computer Science) , Vol. 7941 . Springer , 48 - 60 . Nick Benton, Martin Hofmann, and Vivek Nigam. 2013. Proof-Relevant Logical Relations for Name Generation. In 11th International Conference on Typed Lambda Calculi and Applications (Lecture Notes in Computer Science), Vol. 7941. Springer, 48-60."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535869"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599447"},{"key":"e_1_3_2_1_27_1","first-page":"114","volume-title":"4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8- 10, 2006, Proceedings (Lecture Notes in Computer Science), Naoki Kobayashi (Ed.)","volume":"4279","author":"Benton Nick","year":"2006","unstructured":"Nick Benton , Andrew Kennedy , Martin Hofmann , and Lennart Beringer . 2006 . Reading, Writing and Relations. In Programming Languages and Systems , 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8- 10, 2006, Proceedings (Lecture Notes in Computer Science), Naoki Kobayashi (Ed.) , Vol. 4279 . Springer , 114 - 130 . Nick Benton, Andrew Kennedy, Martin Hofmann, and Lennart Beringer. 2006. Reading, Writing and Relations. In Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8- 10, 2006, Proceedings (Lecture Notes in Computer Science), Naoki Kobayashi (Ed.), Vol. 4279. Springer, 114-130."},{"key":"e_1_3_2_1_28_1","unstructured":"Nick Benton Andrew Kennedy Martin Hofmann and Vivek Nigam. 2016. Counting Successes: Effects and Transformations for Nondeterministic Programs. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Lecture Notes in Computer Science) Sam Lindley Conor McBride Philip W. Trinder and Donald Sannella (Eds.) Vol. 9600. Springer 56-72.  Nick Benton Andrew Kennedy Martin Hofmann and Vivek Nigam. 2016. Counting Successes: Effects and Transformations for Nondeterministic Programs. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Lecture Notes in Computer Science) Sam Lindley Conor McBride Philip W. Trinder and Donald Sannella (Eds.) Vol. 9600. Springer 56-72."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.30"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254086"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2926715"},{"key":"e_1_3_2_1_33_1","first-page":"316","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"\u00c7i\u00e7ek Ezgi","year":"2017","unstructured":"Ezgi \u00c7i\u00e7ek , Gilles Barthe , Marco Gaboardi , Deepak Garg , and Jan Hoffmann . 2017 . Relational cost analysis . In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 , Paris, France , January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 316 - 329 . Ezgi \u00c7i\u00e7ek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2017. Relational cost analysis. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 316-329."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0361-7"},{"key":"e_1_3_2_1_36_1","first-page":"193","volume-title":"Second International Conference, SPC 2005, Boppard, Germany, April 6-8, 2005, Proceedings (Lecture Notes in Computer Science), Dieter Hutter and Markus Ullmann (Eds.)","volume":"3450","author":"Darvas \u00c1d\u00e1m","year":"2005","unstructured":"\u00c1d\u00e1m Darvas , Reiner H\u00e4hnle , and David Sands . 2005 . A Theorem Proving Approach to Analysis of Secure Information Flow. In Security in Pervasive Computing , Second International Conference, SPC 2005, Boppard, Germany, April 6-8, 2005, Proceedings (Lecture Notes in Computer Science), Dieter Hutter and Markus Ullmann (Eds.) , Vol. 3450 . Springer , 193 - 209 . \u00c1d\u00e1m Darvas, Reiner H\u00e4hnle, and David Sands. 2005. A Theorem Proving Approach to Analysis of Secure Information Flow. In Security in Pervasive Computing, Second International Conference, SPC 2005, Boppard, Germany, April 6-8, 2005, Proceedings (Lecture Notes in Computer Science), Dieter Hutter and Markus Ullmann (Eds.), Vol. 3450. Springer, 193-209."},{"key":"e_1_3_2_1_37_1","volume-title":"Logical Step-Indexed Logical Relations. Logical Methods in Computer Science 7, 2","author":"Dreyer Derek","year":"2011","unstructured":"Derek Dreyer , Amal Ahmed , and Lars Birkedal . 2011. Logical Step-Indexed Logical Relations. Logical Methods in Computer Science 7, 2 ( 2011 ). Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011. Logical Step-Indexed Logical Relations. Logical Methods in Computer Science 7, 2 (2011)."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706323"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968604"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_3_2_1_42_1","volume-title":"Time for Verification, Essays in Memory of Amir Pnueli (Lecture Notes in Computer Science), Zohar Manna and Doron A","author":"Godlin Benny","unstructured":"Benny Godlin and Ofer Strichman . 2010. Inference Rules for Proving the Equivalence of Recursive Procedures . In Time for Verification, Essays in Memory of Amir Pnueli (Lecture Notes in Computer Science), Zohar Manna and Doron A . Peled (Eds.), Vol. 6200 . Springer , 167-184. Benny Godlin and Ofer Strichman. 2010. Inference Rules for Proving the Equivalence of Recursive Procedures. In Time for Verification, Essays in Memory of Amir Pnueli (Lecture Notes in Computer Science), Zohar Manna and Doron A. Peled (Eds.), Vol. 6200. Springer, 167-184."},{"key":"e_1_3_2_1_43_1","volume-title":"Security Policies and Security Models. 1982 IEEE Symposium on Security and Privacy 00","author":"Goguen J. A.","year":"1982","unstructured":"J. A. Goguen and J. Meseguer . 1982 . Security Policies and Security Models. 1982 IEEE Symposium on Security and Privacy 00 ( 1982 ), 11. J. A. Goguen and J. Meseguer. 1982. Security Policies and Security Models. 1982 IEEE Symposium on Security and Privacy 00 (1982), 11."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Niklas Grimm Kenji Maillard C\u00e9dric Fournet Catalin Hritcu Matteo Maffei Jonathan Protzenko Tahina Ramananandro Aseem Rastogi Nikhil Swamy and Santiago Zanella-B\u00e9guelin. 2017. A Monadic Framework for Relational Verification: Applied to Information Security Program Equivalence and Optimizations. arXiv:1703.00055. https:\/\/arxiv.org\/abs\/1703.00055.   Niklas Grimm Kenji Maillard C\u00e9dric Fournet Catalin Hritcu Matteo Maffei Jonathan Protzenko Tahina Ramananandro Aseem Rastogi Nikhil Swamy and Santiago Zanella-B\u00e9guelin. 2017. A Monadic Framework for Relational Verification: Applied to Information Security Program Equivalence and Optimizations. arXiv:1703.00055. https:\/\/arxiv.org\/abs\/1703.00055.","DOI":"10.1145\/3167090"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-009-0086-1"},{"key":"e_1_3_2_1_46_1","first-page":"237","volume-title":"NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings (Lecture Notes in Computer Science), Sanjai Rayadurgam and Oksana Tkachuk (Eds.)","volume":"9690","author":"He Shaobo","year":"2016","unstructured":"Shaobo He , Shuvendu K. Lahiri , and Zvonimir Rakamaric . 2016 . Verifying Relative Safety, Accuracy, and Termination for Program Approximations. In NASA Formal Methods - 8th International Symposium , NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings (Lecture Notes in Computer Science), Sanjai Rayadurgam and Oksana Tkachuk (Eds.) , Vol. 9690 . Springer , 237 - 254 . Shaobo He, Shuvendu K. Lahiri, and Zvonimir Rakamaric. 2016. Verifying Relative Safety, Accuracy, and Termination for Program Approximations. In NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings (Lecture Notes in Computer Science), Sanjai Rayadurgam and Oksana Tkachuk (Eds.), Vol. 9690. Springer, 237-254."},{"key":"e_1_3_2_1_47_1","first-page":"319","volume-title":"NATO Science for Peace and Security Series - D: Information and Communication Security","volume":"33","author":"Hedin Daniel","year":"2012","unstructured":"Daniel Hedin and Andrei Sabelfeld . 2012 . A Perspective on Information-Flow Control. In Software Safety and Security - Tools for Analysis and Verification, Tobias Nipkow, Orna Grumberg, and Benedikt Hauptmann (Eds.) . NATO Science for Peace and Security Series - D: Information and Communication Security , Vol. 33 . IOS Press , 319 - 347 . Daniel Hedin and Andrei Sabelfeld. 2012. A Perspective on Information-Flow Control. In Software Safety and Security - Tools for Analysis and Verification, Tobias Nipkow, Orna Grumberg, and Benedikt Hauptmann (Eds.). NATO Science for Peace and Security Series - D: Information and Communication Security, Vol. 33. IOS Press, 319-347."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111050"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542513"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.28"},{"key":"e_1_3_2_1_53_1","first-page":"712","volume-title":"CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science), P. Madhusudan and Sanjit A. Seshia (Eds.)","volume":"7358","author":"Lahiri Shuvendu K.","year":"2012","unstructured":"Shuvendu K. Lahiri , Chris Hawblitzel , Ming Kawaguchi , and Henrique Reb\u00ealo . 2012 . SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs. In Computer Aided Verification - 24th International Conference , CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science), P. Madhusudan and Sanjit A. Seshia (Eds.) , Vol. 7358 . Springer , 712 - 717 . Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, and Henrique Reb\u00ealo. 2012. SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science), P. Madhusudan and Sanjit A. Seshia (Eds.), Vol. 7358. Springer, 712-717."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0319-6"},{"key":"e_1_3_2_1_55_1","first-page":"257","volume-title":"MPC 2015, K\u00f6nigswinter, Germany, June 29 - July 1, 2015. Proceedings (Lecture Notes in Computer Science), Ralf Hinze and Janis Voigtl\u00e4nder (Eds.)","volume":"9129","author":"McBride Conor","year":"2015","unstructured":"Conor McBride . 2015 . Turing-Completeness Totally Free. In Mathematics of Program Construction - 12th International Conference , MPC 2015, K\u00f6nigswinter, Germany, June 29 - July 1, 2015. Proceedings (Lecture Notes in Computer Science), Ralf Hinze and Janis Voigtl\u00e4nder (Eds.) , Vol. 9129 . Springer , 257 - 275 . Conor McBride. 2015. Turing-Completeness Totally Free. In Mathematics of Program Construction - 12th International Conference, MPC 2015, K\u00f6nigswinter, Germany, June 29 - July 1, 2015. Proceedings (Lecture Notes in Computer Science), Ralf Hinze and Janis Voigtl\u00e4nder (Eds.), Vol. 9129. Springer, 257-275."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512669"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77353"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491522.2491523"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/11863908_18"},{"key":"e_1_3_2_1_62_1","first-page":"263","volume-title":"Quotient Types: A Modular Approach. In 15th International Conference on Theorem Proving in Higher Order Logics (Lecture Notes in Computer Science)","volume":"2410","author":"Nogin Aleksey","year":"2002","unstructured":"Aleksey Nogin . 2002 . Quotient Types: A Modular Approach. In 15th International Conference on Theorem Proving in Higher Order Logics (Lecture Notes in Computer Science) , Vol. 2410 . Springer , 263 - 280 . Aleksey Nogin. 2002. Quotient Types: A Modular Approach. In 15th International Conference on Theorem Proving in Higher Order Logics (Lecture Notes in Computer Science), Vol. 2410. Springer, 263-280."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_3_2_1_64_1","volume-title":"Tackling the Awkward Squad: monadic input\/output, concurrency, exceptions, and foreign-language calls in Haskell","author":"Jones Simon Peyton","unstructured":"Simon Peyton Jones . 2010. Tackling the Awkward Squad: monadic input\/output, concurrency, exceptions, and foreign-language calls in Haskell . IOS Press , 47-96. https:\/\/www.microsoft.com\/en-us\/research\/publication\/tackling-awkward-squad-monadic-inputoutput-concurrency-exceptions-foreign-language-calls-haskell\/. Simon Peyton Jones. 2010. Tackling the Awkward Squad: monadic input\/output, concurrency, exceptions, and foreign-language calls in Haskell. IOS Press, 47-96. https:\/\/www.microsoft.com\/en-us\/research\/publication\/tackling-awkward-squad-monadic-inputoutput-concurrency-exceptions-foreign-language-calls-haskell\/."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_1_67_1","first-page":"1","article-title":"Language-based Information-flow Security","volume":"21","author":"Sabelfeld A.","year":"2006","unstructured":"A. Sabelfeld and A. C. Myers . 2006 . Language-based Information-flow Security . IEEE J.Sel. A. Commun. 21 , 1 (Sept. 2006), 5-19. A. Sabelfeld and A. C. Myers. 2006. Language-based Information-flow Security. IEEE J.Sel. A. Commun. 21, 1 (Sept. 2006), 5-19.","journal-title":"IEEE J.Sel. A. Commun."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890002"},{"key":"e_1_3_2_1_69_1","volume-title":"Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2011","author":"Scheben Christoph","year":"2011","unstructured":"Christoph Scheben and Peter H. Schmitt . 2011. Verification of Information Flow Properties of Java Programs without Approximations . In Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2011 , Turin, Italy , October 5-7, 2011 , Revised Selected Papers (Lecture Notes in Computer Science), Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov (Eds.), Vol. 7421. Springer, 232-249. Christoph Scheben and Peter H. Schmitt. 2011. Verification of Information Flow Properties of Java Programs without Approximations. In Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2011, Turin, Italy, October 5-7, 2011, Revised Selected Papers (Lecture Notes in Computer Science), Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov (Eds.), Vol. 7421. Springer, 232-249."},{"key":"e_1_3_2_1_70_1","volume-title":"Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009","author":"Shao Zhong","year":"2009","unstructured":"Zhong Shao and Benjamin C . Pierce (Eds.). 2009 . Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009 , Savannah, GA, USA , January 21-23, 2009 . ACM. http:\/\/dl.acm.org\/citation.cfm?id=1480881. Zhong Shao and Benjamin C. Pierce (Eds.). 2009. Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009. ACM. http:\/\/dl.acm.org\/citation.cfm?id=1480881."},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_2_1_72_1","volume-title":"Computer Science Logic, 23rd international Workshop, CSL","author":"Sumii Eijiro","year":"2009","unstructured":"Eijiro Sumii . 2009. A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References . In Computer Science Logic, 23rd international Workshop, CSL 2009 , 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings (Lecture Notes in Computer Science), Erich Gr\u00e4del and Reinhard Kahle (Eds.), Vol. 5771 . Springer , 455-469. Eijiro Sumii. 2009. A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References. In Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings (Lecture Notes in Computer Science), Erich Gr\u00e4del and Reinhard Kahle (Eds.), Vol. 5771. Springer, 455-469."},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034778"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_2_1_76_1","first-page":"352","volume-title":"12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings (Lecture Notes in Computer Science), Chris Hankin and Igor Siveroni (Eds.)","volume":"3672","author":"Terauchi Tachio","year":"2005","unstructured":"Tachio Terauchi and Alexander Aiken . 2005 . Secure Information Flow as a Safety Problem. In Static Analysis , 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings (Lecture Notes in Computer Science), Chris Hankin and Igor Siveroni (Eds.) , Vol. 3672 . Springer , 352 - 367 . Tachio Terauchi and Alexander Aiken. 2005. Secure Information Flow as a Safety Problem. In Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings (Lecture Notes in Computer Science), Chris Hankin and Igor Siveroni (Eds.), Vol. 3672. Springer, 352-367."},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2013.07.031"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009884"}],"event":{"name":"CPP '18: Certified Proofs and Programs","location":"Los Angeles CA USA","acronym":"CPP '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167090","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:28Z","timestamp":1750212808000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167090"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":79,"alternative-id":["10.1145\/3167090","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167090","relation":{},"subject":[],"published":{"date-parts":[[2018,1,8]]},"assertion":[{"value":"2018-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}