{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:35:52Z","timestamp":1774838152905,"version":"3.50.1"},"reference-count":70,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1911149"],"award-info":[{"award-number":["1911149"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,8,2]]},"abstract":"<jats:p>We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, thereby easing the programmer burden of implementing policy enforcing code throughout the application.<\/jats:p><jats:p>The main insight behind Lifty is to encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking of complex, data dependent policies, and power our repair mechanism via type-driven error localization and patch synthesis. Our experience using Lifty to implement three case studies from the literature shows that (1) the Lifty policy language is sufficiently expressive to specify many real-world policies, (2) the Lifty type checker is able to verify secure programs and find leaks in insecure programs quickly, and (3) even if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time.<\/jats:p>","DOI":"10.1145\/3408987","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T13:48:02Z","timestamp":1596462482000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Liquid information flow control"],"prefix":"10.1145","volume":"4","author":[{"given":"Nadia","family":"Polikarpova","sequence":"first","affiliation":[{"name":"University of California at San Diego, USA"}]},{"given":"Deian","family":"Stefan","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]},{"given":"Jean","family":"Yang","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Shachar","family":"Itzhaky","sequence":"additional","affiliation":[{"name":"Technion, Israel"}]},{"given":"Travis","family":"Hance","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Armando","family":"Solar-Lezama","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_2_1_1","first-page":"319","article-title":"Scaling Enumerative Program Synthesis via Divide and Conquer","author":"Alur Rajeev","year":"2017","unstructured":"Rajeev Alur , Arjun Radhakrishna , and Abhishek Udupa . 2017 . Scaling Enumerative Program Synthesis via Divide and Conquer . In TACAS. 319 - 336 . Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer. In TACAS. 319-336.","journal-title":"TACAS."},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"O. Arden M. D. George J. Liu K. Vikram A. Askarov and A. C. Myers. 2012. Sharing Mobile Code Securely with Information Flow Control. In Oakland. O. Arden M. D. George J. Liu K. Vikram A. Askarov and A. C. Myers. 2012. Sharing Mobile Code Securely with Information Flow Control. In Oakland.","DOI":"10.1109\/SP.2012.22"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"Thomas H. Austin Jean Yang Cormac Flanagan and Armando Solar-Lezama. 2013. Faceted execution of policy-agnostic programs. In PLAS. Thomas H. Austin Jean Yang Cormac Flanagan and Armando Solar-Lezama. 2013. Faceted execution of policy-agnostic programs. In PLAS.","DOI":"10.1145\/2465106.2465121"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-15791"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784758"},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Juan Chen Ravi Chugh and Nikhil Swamy. 2010. Type-preserving compilation of end-to-end verification of security enforcement. In PLDI. Juan Chen Ravi Chugh and Nikhil Swamy. 2010. Type-preserving compilation of end-to-end verification of security enforcement. In PLDI.","DOI":"10.1145\/1806596.1806643"},{"key":"e_1_2_2_7_1","unstructured":"Adam Chlipala. 2010. Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. In OSDI. Adam Chlipala. 2010. Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. In OSDI."},{"key":"e_1_2_2_8_1","unstructured":"Catalin Cimpanu. 2020. Walgreens says mobile app leaked users' personal data. https:\/\/www.zdnet.com\/article\/walgreenssays-mobile-app-leaked-users-personal-data\/. Catalin Cimpanu. 2020. Walgreens says mobile app leaked users' personal data. https:\/\/www.zdnet.com\/article\/walgreenssays-mobile-app-leaked-users-personal-data\/."},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Benjamin Cosman and Ranjit Jhala. 2017. Local refinement typing. PACMPL 1 ICFP ( 2017 ) 26 : 1-26 : 27. Benjamin Cosman and Ranjit Jhala. 2017. Local refinement typing. PACMPL 1 ICFP ( 2017 ) 26 : 1-26 : 27.","DOI":"10.1145\/3110270"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005441"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929553.1929564"},{"key":"e_1_2_2_12_1","first-page":"684","article-title":"Explain: A Tool for Performing Abductive Inference","author":"Dillig Isil","year":"2013","unstructured":"Isil Dillig and Thomas Dillig . 2013 . Explain: A Tool for Performing Abductive Inference . In CAV. 684 - 689 . Isil Dillig and Thomas Dillig. 2013. Explain: A Tool for Performing Abductive Inference. In CAV. 684-689.","journal-title":"CAV."},{"key":"e_1_2_2_13_1","unstructured":"Cory Doctorow. 2015. United website breach let fliers see each others' private data. https:\/\/boingboing.net\/ 2015 \/01\/28\/unitedwebsite-breach-let-flie.html. Cory Doctorow. 2015. United website breach let fliers see each others' private data. https:\/\/boingboing.net\/ 2015 \/01\/28\/unitedwebsite-breach-let-flie.html."},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Matthew Fredrikson Richard Joiner Somesh Jha Thomas W. Reps Phillip A. Porras Hassen Sa\u00efdi and Vinod Yegneswaran. 2012. Eficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement. In CAV. Matthew Fredrikson Richard Joiner Somesh Jha Thomas W. Reps Phillip A. Porras Hassen Sa\u00efdi and Vinod Yegneswaran. 2012. Eficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement. In CAV.","DOI":"10.1007\/978-3-642-31424-7_39"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Vinod Ganapathy Trent Jaeger and Somesh Jha. 2006. Retrofitting Legacy Code for Authorization Policy Enforcement. In SP. Vinod Ganapathy Trent Jaeger and Somesh Jha. 2006. Retrofitting Legacy Code for Authorization Policy Enforcement. In SP.","DOI":"10.1109\/SP.2006.34"},{"key":"e_1_2_2_16_1","volume-title":"Hails: Protecting Data Privacy in Untrusted Web Applications. Journal of Computer Security 25 ( 2017 ).","author":"Gifin Daniel B.","year":"2017","unstructured":"Daniel B. Gifin , Amit Levy , Deian Stefan , David Terei , David Mazi\u00e8res , John Mitchell , and Alejandro Russo . 2017 . Hails: Protecting Data Privacy in Untrusted Web Applications. Journal of Computer Security 25 ( 2017 ). Daniel B. Gifin, Amit Levy, Deian Stefan, David Terei, David Mazi\u00e8res, John Mitchell, and Alejandro Russo. 2017. Hails: Protecting Data Privacy in Untrusted Web Applications. Journal of Computer Security 25 ( 2017 )."},{"key":"e_1_2_2_17_1","first-page":"47","article-title":"Hails","author":"Gifin Daniel B.","year":"2012","unstructured":"Daniel B. Gifin , Amit Levy , Deian Stefan , David Terei , David Mazi\u00e8res , John C. Mitchell , and Alejandro Russo . 2012 . Hails : Protecting Data Privacy in Untrusted Web Applications. In OSDI. 47 - 60 . Daniel B. Gifin, Amit Levy, Deian Stefan, David Terei, David Mazi\u00e8res, John C. Mitchell, and Alejandro Russo. 2012. Hails: Protecting Data Privacy in Untrusted Web Applications. In OSDI. 47-60.","journal-title":"Protecting Data Privacy in Untrusted Web Applications. In OSDI."},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"William R. Harris Somesh Jha and Thomas Reps. 2010. DIFC Programs by Automatic Instrumentation. In CCS. William R. Harris Somesh Jha and Thomas Reps. 2010. DIFC Programs by Automatic Instrumentation. In CCS.","DOI":"10.1145\/1866307.1866340"},{"key":"e_1_2_2_19_1","unstructured":"Kashmir Hill. 2017. How Facebook Outs Sex Workers. https:\/\/gizmodo.com \/how-facebook-outs-sex-workers-1818861596 Kashmir Hill. 2017. How Facebook Outs Sex Workers. https:\/\/gizmodo.com \/how-facebook-outs-sex-workers-1818861596"},{"key":"e_1_2_2_20_1","first-page":"73","article-title":"Optimizing horn solvers for network repair","author":"Hojjat Hossein","year":"2016","unstructured":"Hossein Hojjat , Philipp R\u00fcmmer , Jedidiah McClurg , Pavol Cern\u00fd , and Nate Foster . 2016 . Optimizing horn solvers for network repair . In FMCAD. 73 - 80 . Hossein Hojjat, Philipp R\u00fcmmer, Jedidiah McClurg, Pavol Cern\u00fd, and Nate Foster. 2016. Optimizing horn solvers for network repair. In FMCAD. 73-80.","journal-title":"FMCAD."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"e_1_2_2_22_1","unstructured":"Troy Hunt. 2020. Have I Been Pwned: Check if your email has been compromised in a data breach. https:\/\/haveibeenpwned. com\/. Troy Hunt. 2020. Have I Been Pwned: Check if your email has been compromised in a data breach. https:\/\/haveibeenpwned. com\/."},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Limin Jia and Steve Zdancewic. 2009. Encoding information flow in Aura. In PLAS. Limin Jia and Steve Zdancewic. 2009. Encoding information flow in Aura. In PLAS.","DOI":"10.1145\/1554339.1554344"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Etienne Kneuss Manos Koukoutos and Viktor Kuncak. 2015. Deductive Program Repair. In CAV. Etienne Kneuss Manos Koukoutos and Viktor Kuncak. 2015. Deductive Program Repair. In CAV.","DOI":"10.1007\/978-3-319-21668-3_13"},{"key":"e_1_2_2_25_1","first-page":"407","article-title":"Synthesis modulo recursive functions","author":"Kneuss Etienne","year":"2013","unstructured":"Etienne Kneuss , Ivan Kuraj , Viktor Kuncak , and Philippe Suter . 2013 . Synthesis modulo recursive functions . In OOPSLA. 407 - 426 . Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. 2013. Synthesis modulo recursive functions. In OOPSLA. 407-426.","journal-title":"OOPSLA."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"Viktor Kuncak Mika\u00ebl Mayer Ruzica Piskac and Philippe Suter. 2010. Complete functional synthesis. In PLDI. Viktor Kuncak Mika\u00ebl Mayer Ruzica Piskac and Philippe Suter. 2010. Complete functional synthesis. In PLDI.","DOI":"10.1145\/1806596.1806632"},{"key":"e_1_2_2_28_1","unstructured":"Peng Li and Steve Zdancewic. 2005. Downgrading Policies and Relaxed Noninterference. ( 2005 ). Peng Li and Steve Zdancewic. 2005. Downgrading Policies and Relaxed Noninterference. ( 2005 )."},{"key":"e_1_2_2_29_1","unstructured":"Peng Li and Steve Zdancewic. 2006. Encoding Information Flow in Haskell. In CSFW. Peng Li and Steve Zdancewic. 2006. Encoding Information Flow in Haskell. In CSFW."},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"J. Liu M. D. George K. Vikram X. Qi L. Waye and A. C. Myers. 2009. Fabric: a platform for secure distributed computation and storage. In SOSP. ACM. J. Liu M. D. George K. Vikram X. Qi L. Waye and A. C. Myers. 2009. Fabric: a platform for secure distributed computation and storage. In SOSP. ACM.","DOI":"10.1145\/1629575.1629606"},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"Calvin Loncaric Satish Chandra Cole Schlesinger and Manu Sridharan. 2016. A Practical Framework for Type Inference Error Explanation. In OOPSLA. ACM. Calvin Loncaric Satish Chandra Cole Schlesinger and Manu Sridharan. 2016. A Practical Framework for Type Inference Error Explanation. In OOPSLA. ACM.","DOI":"10.1145\/2983990.2983994"},{"key":"e_1_2_2_32_1","volume-title":"Trustworthy Global Computing","author":"Louren\u00e7o Lu\u00edsa","unstructured":"Lu\u00edsa Louren\u00e7o and Lu\u00eds Caires . 2014. Information flow analysis for valued-indexed data security compartments . In Trustworthy Global Computing . Springer , 180-198. Lu\u00edsa Louren\u00e7o and Lu\u00eds Caires. 2014. Information flow analysis for valued-indexed data security compartments. In Trustworthy Global Computing. Springer, 180-198."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676994"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"e_1_2_2_35_1","unstructured":"Simon Marlow. 2010. Haskell 2010 language report. https:\/\/www.haskell.org\/onlinereport\/haskell2010\/ Simon Marlow. 2010. Haskell 2010 language report. https:\/\/www.haskell.org\/onlinereport\/haskell2010\/"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"Beno\u00eet Montagu Benjamin C. Pierce and Randy Pollack. 2013. A Theory of Information-Flow Labels. In CSF. Beno\u00eet Montagu Benjamin C. Pierce and Randy Pollack. 2013. A Theory of Information-Flow Labels. In CSF.","DOI":"10.1109\/CSF.2013.8"},{"key":"e_1_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Andrew C. Myers. 1999. JFlow: Practical Mostly-Static Information Flow Control. In POPL. Andrew C. Myers. 1999. JFlow: Practical Mostly-Static Information Flow Control. In POPL.","DOI":"10.1145\/292540.292561"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363526"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290388"},{"key":"e_1_2_2_40_1","unstructured":"S. Peyton Jones. 2001. Tackling the awkward squad: monadic input\/output concurrency exceptions and foreign-language calls in Haskell. Engineering theories of software construction 180 ( 2001 ) 47. S. Peyton Jones. 2001. Tackling the awkward squad: monadic input\/output concurrency exceptions and foreign-language calls in Haskell. Engineering theories of software construction 180 ( 2001 ) 47."},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"Nadia Polikarpova Ivan Kuraj and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types. In PLDI. Nadia Polikarpova Ivan Kuraj and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types. In PLDI.","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_2_42_1","unstructured":"Nadia Polikarpova Deian Stefan Jean Yang Shachar Itzhaky Travis Hance and Armando Solar-Lezama. 2020. Liquid Information Flow Control. CoRR abs\/1607.03445 ( 2020 ). arXiv: 1607.03445 http:\/\/arxiv.org\/abs\/1607.03445 Nadia Polikarpova Deian Stefan Jean Yang Shachar Itzhaky Travis Hance and Armando Solar-Lezama. 2020. Liquid Information Flow Control. CoRR abs\/1607.03445 ( 2020 ). arXiv: 1607.03445 http:\/\/arxiv.org\/abs\/1607.03445"},{"key":"e_1_2_2_43_1","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1145\/503272.503302","article-title":"Information flow inference for ML","author":"Pottier Fran\u00e7ois","year":"2002","unstructured":"Fran\u00e7ois Pottier and Vincent Simonet . 2002 . Information flow inference for ML . In POPL. 319 - 330 . Fran\u00e7ois Pottier and Vincent Simonet. 2002. Information flow inference for ML. In POPL. 319-330.","journal-title":"POPL."},{"key":"e_1_2_2_44_1","unstructured":"Privacy Rights Clearinghouse. 2020. Data Breaches. https:\/\/www.privacyrights.org\/data-breach\/. Privacy Rights Clearinghouse. 2020. Data Breaches. https:\/\/www.privacyrights.org\/data-breach\/."},{"key":"e_1_2_2_45_1","doi-asserted-by":"crossref","unstructured":"Vineet Rajani and Deepak Garg. 2020. On the expressiveness and semantics of information flow types. Journal of Computer Security 28 ( 2020 ). Vineet Rajani and Deepak Garg. 2020. On the expressiveness and semantics of information flow types. Journal of Computer Security 28 ( 2020 ).","DOI":"10.3233\/JCS-191382"},{"key":"e_1_2_2_46_1","unstructured":"Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid types. In PLDI. Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid types. In PLDI."},{"key":"e_1_2_2_47_1","volume-title":"Functional Pearl: Two Can Keep a Secret, If One of Them Uses Haskell. In ICFP.","author":"Russo Alejandro","year":"2015","unstructured":"Alejandro Russo . 2015 . Functional Pearl: Two Can Keep a Secret, If One of Them Uses Haskell. In ICFP. Alejandro Russo. 2015. Functional Pearl: Two Can Keep a Secret, If One of Them Uses Haskell. In ICFP."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411289"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_2_50_1","doi-asserted-by":"crossref","unstructured":"Eric L. Seidel Huma Sibghat Kamalika Chaudhuri Westley Weimer and Ranjit Jhala. 2017. Learning to blame: localizing novice type errors with data-driven diagnosis. PACMPL 1 OOPSLA ( 2017 ) 60 : 1-60 : 27. Eric L. Seidel Huma Sibghat Kamalika Chaudhuri Westley Weimer and Ranjit Jhala. 2017. Learning to blame: localizing novice type errors with data-driven diagnosis. PACMPL 1 OOPSLA ( 2017 ) 60 : 1-60 : 27.","DOI":"10.1145\/3138818"},{"key":"e_1_2_2_51_1","first-page":"249","article-title":"Logical attestation: an authorization architecture for trustworthy computing","author":"Sirer E.G.","year":"2011","unstructured":"E.G. Sirer , W. de Bruijn , P. Reynolds , A. Shieh , K. Walsh , D. Williams , and F.B. Schneider . 2011 . Logical attestation: an authorization architecture for trustworthy computing . In SOSP. 249 - 264 . E.G. Sirer, W. de Bruijn, P. Reynolds, A. Shieh, K. Walsh, D. Williams, and F.B. Schneider. 2011. Logical attestation: an authorization architecture for trustworthy computing. In SOSP. 249-264.","journal-title":"SOSP."},{"key":"e_1_2_2_52_1","volume-title":"Fix Me Up: Repairing Access-Control Bugs in Web Applications","author":"Son Sooel","unstructured":"Sooel Son , Kathryn S. McKinley , and Vitaly Shmatikov . 2013. Fix Me Up: Repairing Access-Control Bugs in Web Applications . In NDSS. The Internet Society . Sooel Son, Kathryn S. McKinley, and Vitaly Shmatikov. 2013. Fix Me Up: Repairing Access-Control Bugs in Web Applications. In NDSS. The Internet Society."},{"key":"e_1_2_2_53_1","doi-asserted-by":"crossref","unstructured":"Deian Stefan David Mazi\u00e8res John C. Mitchell and Alejandro Russo. 2017. Flexible dynamic information flow control in the presence of exceptions. J. Funct. Program. 27 ( 2017 ). Deian Stefan David Mazi\u00e8res John C. Mitchell and Alejandro Russo. 2017. Flexible dynamic information flow control in the presence of exceptions. J. Funct. Program. 27 ( 2017 ).","DOI":"10.1017\/S0956796816000241"},{"key":"e_1_2_2_54_1","volume-title":"Mitchell","author":"Stefan Deian","year":"2011","unstructured":"Deian Stefan , Alejandro Russo , David Mazi\u00e8res , and John C . Mitchell . 2011 a. Disjunction Category Labels. In Nordic Conference on Security IT Systems (NordSec). Springer . Deian Stefan, Alejandro Russo, David Mazi\u00e8res, and John C. Mitchell. 2011a. Disjunction Category Labels. In Nordic Conference on Security IT Systems (NordSec). Springer."},{"key":"e_1_2_2_55_1","volume-title":"Flexible Dynamic Information Flow Control in Haskell. In Haskell Symposium. ACM SIGPLAN.","author":"Stefan Deian","year":"2011","unstructured":"Deian Stefan , Alejandro Russo , John C. Mitchell , and David Mazi\u00e8res . 2011 b. Flexible Dynamic Information Flow Control in Haskell. In Haskell Symposium. ACM SIGPLAN. Deian Stefan, Alejandro Russo, John C. Mitchell, and David Mazi\u00e8res. 2011b. Flexible Dynamic Information Flow Control in Haskell. In Haskell Symposium. ACM SIGPLAN."},{"key":"e_1_2_2_56_1","doi-asserted-by":"crossref","unstructured":"Nikhil Swamy Juan Chen and Ravi Chugh. 2010. Enforcing Stateful Authorization and Information Flow Policies in Fine. In ESOP. Nikhil Swamy Juan Chen and Ravi Chugh. 2010. Enforcing Stateful Authorization and Information Flow Policies in Fine. In ESOP.","DOI":"10.1007\/978-3-642-11957-6_28"},{"key":"e_1_2_2_57_1","doi-asserted-by":"crossref","unstructured":"Nikhil Swamy Juan Chen C\u00e9dric Fournet Pierre-Yves Strub Karthikeyan Bhargavan and Jean Yang. 2011. Secure distributed programming with value-dependent types. In ICFP. Nikhil Swamy Juan Chen C\u00e9dric Fournet Pierre-Yves Strub Karthikeyan Bhargavan and Jean Yang. 2011. Secure distributed programming with value-dependent types. In ICFP.","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_2_2_58_1","volume-title":"Bierman","author":"Swamy Nikhil","year":"2009","unstructured":"Nikhil Swamy , Michael Hicks , and Gavin M . Bierman . 2009 . A Theory of Typed Coercions and Its Applications. In ICFP. ACM. Nikhil Swamy, Michael Hicks, and Gavin M. Bierman. 2009. A Theory of Typed Coercions and Its Applications. In ICFP. ACM."},{"key":"e_1_2_2_59_1","first-page":"15","article-title":"On Formalizing Information-Flow Control Libraries. In PLAS, Toby C. Murray and Deian Stefan (Eds.)","author":"Vassena Marco","year":"2016","unstructured":"Marco Vassena and Alejandro Russo . 2016 . On Formalizing Information-Flow Control Libraries. In PLAS, Toby C. Murray and Deian Stefan (Eds.) . ACM , 15 - 28 . Marco Vassena and Alejandro Russo. 2016. On Formalizing Information-Flow Control Libraries. In PLAS, Toby C. Murray and Deian Stefan (Eds.). ACM, 15-28.","journal-title":"ACM"},{"key":"e_1_2_2_60_1","doi-asserted-by":"crossref","unstructured":"Marco Vassena Alejandro Russo Pablo Buiras and Lucas Waye. 2018. MAC: a verified static information-flow control library. Journal of logical and algebraic methods in programming 95 ( 2018 ) 148-180. Marco Vassena Alejandro Russo Pablo Buiras and Lucas Waye. 2018. MAC: a verified static information-flow control library. Journal of logical and algebraic methods in programming 95 ( 2018 ) 148-180.","DOI":"10.1016\/j.jlamp.2017.12.003"},{"key":"e_1_2_2_61_1","volume-title":"Patrick Maxim Rondon, and Ranjit Jhala","author":"Vazou Niki","year":"2013","unstructured":"Niki Vazou , Patrick Maxim Rondon, and Ranjit Jhala . 2013 . Abstract Refinement Types. In ESOP. Niki Vazou, Patrick Maxim Rondon, and Ranjit Jhala. 2013. Abstract Refinement Types. In ESOP."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_2_2_63_1","volume-title":"Peyton Jones","author":"Vazou Niki","year":"2014","unstructured":"Niki Vazou , Eric L. Seidel , Ranjit Jhala , Dimitrios Vytiniotis , and Simon L . Peyton Jones . 2014 b. Refinement types for Haskell. In ICFP. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014b. Refinement types for Haskell. In ICFP."},{"key":"e_1_2_2_64_1","unstructured":"Chelsea Voss. 2016. private email communication. Chelsea Voss. 2016. private email communication."},{"key":"e_1_2_2_65_1","unstructured":"Jean Yang. 2017. James Comey's Twitter Security Problem Is Your Problem Too. https:\/\/www.technologyreview.com\/s\/ 604286\/james-comeys-twitter-security-problem-is-your-problem-too Jean Yang. 2017. James Comey's Twitter Security Problem Is Your Problem Too. https:\/\/www.technologyreview.com\/s\/ 604286\/james-comeys-twitter-security-problem-is-your-problem-too"},{"key":"e_1_2_2_66_1","doi-asserted-by":"crossref","unstructured":"Jean Yang Travis Hance Thomas H. Austin Armando Solar-Lezama Cormac Flanagan and Stephen Chong. 2016. Precise Dynamic Information Flow for Database-backed Applications. In PLDI. Jean Yang Travis Hance Thomas H. Austin Armando Solar-Lezama Cormac Flanagan and Stephen Chong. 2016. Precise Dynamic Information Flow for Database-backed Applications. In PLDI.","DOI":"10.1145\/2908080.2908098"},{"key":"e_1_2_2_67_1","doi-asserted-by":"crossref","unstructured":"Jean Yang Kuat Yessenov and Armando Solar-Lezama. 2012. A language for automatically enforcing privacy policies. Jean Yang Kuat Yessenov and Armando Solar-Lezama. 2012. A language for automatically enforcing privacy policies.","DOI":"10.1145\/2103656.2103669"},{"key":"e_1_2_2_68_1","unstructured":"Alexander Yip Xi Wang Nickolai Zeldovich and M. Frans Kaashoek. 2009. Improving application security with data flow assertions. SOSP ( 2009 ). Alexander Yip Xi Wang Nickolai Zeldovich and M. Frans Kaashoek. 2009. Improving application security with data flow assertions. SOSP ( 2009 )."},{"key":"e_1_2_2_69_1","doi-asserted-by":"crossref","unstructured":"Danfeng Zhang Andrew C. Myers Dimitrios Vytiniotis and Simon Peyton-Jones. 2015. Diagnosing type errors with class. In PLDI. Danfeng Zhang Andrew C. Myers Dimitrios Vytiniotis and Simon Peyton-Jones. 2015. Diagnosing type errors with class. In PLDI.","DOI":"10.1145\/2737924.2738009"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0019-9"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408987","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408987","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408987","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:59Z","timestamp":1750193279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408987"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":70,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3408987"],"URL":"https:\/\/doi.org\/10.1145\/3408987","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}