{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T14:59:17Z","timestamp":1769353157978,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"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":["1718220"],"award-info":[{"award-number":["1718220"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314603","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"533-547","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Bidirectional type checking for relational properties"],"prefix":"10.1145","author":[{"given":"Ezgi","family":"\u00c7i\u00e7ek","sequence":"first","affiliation":[{"name":"Facebook, USA"}]},{"given":"Weihao","family":"Qu","sequence":"additional","affiliation":[{"name":"SUNY Buffalo, USA"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI for Security and Privacy, Germany \/ IMDEA Software Institute, Spain"}]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[{"name":"SUNY Buffalo, USA"}]},{"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","first-page":"157","article-title":"Formal Parametric Polymorphism","author":"Abadi Mart\u00edn","year":"1993","unstructured":"Mart\u00edn Abadi , Luca Cardelli , and Pierre-Louis Curien . 1993 . Formal Parametric Polymorphism . In Proc. POPL. 157 - 170 . Mart\u00edn Abadi, Luca Cardelli, and Pierre-Louis Curien. 1993. Formal Parametric Polymorphism. In Proc. POPL. 157-170.","journal-title":"Proc. POPL."},{"key":"e_1_3_2_2_2_1","volume-title":"On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1","author":"Abel Andreas","year":"2012","unstructured":"Andreas Abel and Gabriel Scherer . 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1 ( 2012 ). Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1 (2012)."},{"key":"e_1_3_2_2_3_1","volume-title":"ICFP","author":"Abel Andreas","year":"2017","unstructured":"Andreas Abel , Andrea Vezzosi , and Th\u00e9o Winterhalter . 2017. Normalization by evaluation for sized dependent types. PACMPL 1 , ICFP ( 2017 ), 33:1-33:30. Andreas Abel, Andrea Vezzosi, and Th\u00e9o Winterhalter. 2017. Normalization by evaluation for sized dependent types. PACMPL 1, ICFP (2017), 33:1-33:30."},{"key":"e_1_3_2_2_4_1","first-page":"214","article-title":"Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus","author":"Aguirre Alejandro","year":"2018","unstructured":"Alejandro Aguirre , Gilles Barthe , Lars Birkedal , Ales Bizjak , Marco Gaboardi , and Deepak Garg . 2018 . Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus . In Proc. ESOP. 214 - 241 . Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, and Deepak Garg. 2018. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In Proc. ESOP. 214-241.","journal-title":"Proc. ESOP."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_3_2_2_6_1","first-page":"193","article-title":"Probabilistic relational verification for cryptographic implementations","author":"Barthe Gilles","year":"2014","unstructured":"Gilles Barthe , C\u00e9dric Fournet , Benjamin Gr\u00e9goire , Pierre-Yves Strub , Nikhil Swamy , and Santiago Zanella B\u00e9guelin . 2014 . Probabilistic relational verification for cryptographic implementations . In Proc. POPL. 193 - 206 . Gilles Barthe, C\u00e9dric Fournet, Benjamin Gr\u00e9goire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella B\u00e9guelin. 2014. Probabilistic relational verification for cryptographic implementations. In Proc. POPL. 193-206.","journal-title":"Proc. POPL."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_3_2_2_8_1","first-page":"479","article-title":"Lost in translation: Formalizing proposed extensions to C#","author":"Bierman Gavin M.","year":"2007","unstructured":"Gavin M. Bierman , Erik Meijer , and Mads Torgersen . 2007 . Lost in translation: Formalizing proposed extensions to C# . In Proc. OOPSLA. 479 - 498 . Gavin M. Bierman, Erik Meijer, and Mads Torgersen. 2007. Lost in translation: Formalizing proposed extensions to C#. In Proc. OOPSLA. 479-498.","journal-title":"Proc. OOPSLA."},{"key":"e_1_3_2_2_9_1","unstructured":"Fran\u00e7ois Bobot Sylvain Conchon E Contejean Mohamed Iguernelala St\u00e9phane Lescuyer and Alain Mebsout. 2013. The Alt-Ergo automated theorem prover. http:\/\/alt-ergo.lri.fr\/.  Fran\u00e7ois Bobot Sylvain Conchon E Contejean Mohamed Iguernelala St\u00e9phane Lescuyer and Alain Mebsout. 2013. The Alt-Ergo automated theorem prover. http:\/\/alt-ergo.lri.fr\/."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286957"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"e_1_3_2_2_12_1","first-page":"351","article-title":"A Core Quantitative Coeffect Calculus","author":"Brunel Alo\u00efs","year":"2014","unstructured":"Alo\u00efs Brunel , Marco Gaboardi , Damiano Mazza , and Steve Zdancewic . 2014 . A Core Quantitative Coeffect Calculus . In Proc. ESOP. 351 - 370 . Alo\u00efs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Proc. ESOP. 351-370.","journal-title":"Proc. ESOP."},{"key":"e_1_3_2_2_13_1","volume-title":"Proc. POPL. 316-329","author":"\u00c7i\u00e7ek Ezgi","year":"2017","unstructured":"Ezgi \u00c7i\u00e7ek , Gilles Barthe , Marco Gaboardi , Deepak Garg , and Jan Hoffmann . 2017 . Relational Cost Analysis . In Proc. POPL. 316-329 . Ezgi \u00c7i\u00e7ek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2017. Relational Cost Analysis. In Proc. POPL. 316-329."},{"key":"e_1_3_2_2_14_1","first-page":"406","article-title":"Refinement Types for Incremental Computational Complexity","author":"\u00c7i\u00e7ek Ezgi","year":"2015","unstructured":"Ezgi \u00c7i\u00e7ek , Deepak Garg , and Umut A. Acar . 2015 . Refinement Types for Incremental Computational Complexity . In Proc. ESOP. 406 - 431 . Ezgi \u00c7i\u00e7ek, Deepak Garg, and Umut A. Acar. 2015. Refinement Types for Incremental Computational Complexity. In Proc. ESOP. 406-431.","journal-title":"Proc. ESOP."},{"key":"e_1_3_2_2_15_1","first-page":"132","article-title":"A Type Theory for Incremental Computational Complexity With Control Flow Changes","author":"\u00c7i\u00e7ek Ezgi","year":"2016","unstructured":"Ezgi \u00c7i\u00e7ek , Zoe Paraskevopoulou , and Deepak Garg . 2016 . A Type Theory for Incremental Computational Complexity With Control Flow Changes . In Proc. ICFP. 132 - 145 . Ezgi \u00c7i\u00e7ek, Zoe Paraskevopoulou, and Deepak Garg. 2016. A Type Theory for Incremental Computational Complexity With Control Flow Changes. In Proc. ICFP. 132-145.","journal-title":"Proc. ICFP."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00021-6"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351247"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_3_2_2_19_1","first-page":"167","article-title":"The Geometry of Types","author":"Lago Ugo Dal","year":"2013","unstructured":"Ugo Dal Lago and Barbara Petit . 2013 . The Geometry of Types . In Proc. POPL. 167 - 178 . Ugo Dal Lago and Barbara Petit. 2013. The Geometry of Types. In Proc. POPL. 167-178.","journal-title":"Proc. POPL."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746335"},{"key":"e_1_3_2_2_22_1","first-page":"429","article-title":"Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism","author":"Dunfield Joshua","year":"2013","unstructured":"Joshua Dunfield and Neelakantan R. Krishnaswami . 2013 . Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism . In Proc. ICFP. 429 - 442 . Joshua Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism. In Proc. ICFP. 429-442.","journal-title":"Proc. ICFP."},{"key":"e_1_3_2_2_23_1","volume-title":"Krishnaswami","author":"Dunfield Joshua","year":"2019","unstructured":"Joshua Dunfield and Neelakantan R . Krishnaswami . 2019 . Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. PACMPL 3, POPL ( 2019), 9:1-9:28. Joshua Dunfield and Neelakantan R. Krishnaswami. 2019. Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. PACMPL 3, POPL (2019), 9:1-9:28."},{"key":"e_1_3_2_2_24_1","first-page":"250","article-title":"Type Assignment for Intersections and Unions in Call-by-value Languages","author":"Dunfield Joshua","year":"2003","unstructured":"Joshua Dunfield and Frank Pfenning . 2003 . Type Assignment for Intersections and Unions in Call-by-value Languages . In Proc. FOSSACS. 250 - 266 . Joshua Dunfield and Frank Pfenning. 2003. Type Assignment for Intersections and Unions in Call-by-value Languages. In Proc. FOSSACS. 250-266.","journal-title":"Proc. FOSSACS."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90036-W"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_2_27_1","first-page":"357","article-title":"Linear Dependent Types for Differential Privacy","author":"Gaboardi Marco","year":"2013","unstructured":"Marco Gaboardi , Andreas Haeberlen , Justin Hsu , Arjun Narayan , and Benjamin C. Pierce . 2013 . Linear Dependent Types for Differential Privacy . In Proc. POPL. 357 - 370 . Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. 2013. Linear Dependent Types for Differential Privacy. In Proc. POPL. 357-370.","journal-title":"Proc. POPL."},{"key":"e_1_3_2_2_29_1","first-page":"500","article-title":"Do Be Do Be Do","author":"Lindley Sam","year":"2017","unstructured":"Sam Lindley , Conor McBride , and Craig McLaughlin . 2017 . Do Be Do Be Do . In Proc. POPL. 500 - 514 . Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do Be Do Be Do. In Proc. POPL. 500-514.","journal-title":"Proc. POPL."},{"key":"e_1_3_2_2_30_1","first-page":"47","article-title":"Polymorphic Effect Systems","author":"Lucassen J. M.","year":"1988","unstructured":"J. M. Lucassen and D. K. Gifford . 1988 . Polymorphic Effect Systems . In Proc. POPL. 47 - 57 . J. M. Lucassen and D. K. Gifford. 1988. Polymorphic Effect Systems. In Proc. POPL. 47-57.","journal-title":"Proc. POPL."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.12"},{"key":"e_1_3_2_2_32_1","series-title":"Lecture Notes in Computer Science","volume-title":"Correct System Design","author":"Nielson Flemming","unstructured":"Flemming Nielson and HanneRiis Nielson . 1999. Type and Effect Systems . In Correct System Design . Lecture Notes in Computer Science , Vol. 1710 . Springer-Verlag , 114-136. Flemming Nielson and HanneRiis Nielson. 1999. Type and Effect Systems. In Correct System Design. Lecture Notes in Computer Science, Vol. 1710. Springer-Verlag, 114-136."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360207"},{"key":"e_1_3_2_2_34_1","first-page":"385","article-title":"Coeffects: Unified Static Analysis of Context-Dependence","author":"Petricek Tomas","year":"2013","unstructured":"Tomas Petricek , Dominic A. Orchard , and Alan Mycroft . 2013 . Coeffects: Unified Static Analysis of Context-Dependence . In Proc. ICALP. 385 - 397 . Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. 2013. Coeffects: Unified Static Analysis of Context-Dependence. In Proc. ICALP. 385-397.","journal-title":"Proc. ICALP."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"e_1_3_2_2_39_1","first-page":"266","article-title":"Secure distributed programming with value-dependent types","author":"Swamy Nikhil","year":"2011","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 Proc. ICFP. 266 - 278 . Nikhil Swamy, Juan Chen, C\u00e9dric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure distributed programming with value-dependent types. In Proc. ICFP. 266-278.","journal-title":"Proc. ICFP."},{"key":"e_1_3_2_2_40_1","first-page":"256","article-title":"Dependent types and multi-monadic effects in F*","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy , Catalin Hritcu , Chantal Keller , Aseem Rastogi , Antoine Delignat-Lavaud , Simon Forest , Karthikeyan Bhargavan , C\u00e9dric Fournet , Pierre-Yves Strub , Markulf Kohlweiss , Jean Karim Zinzindohoue , and Santiago Zanella B\u00e9guelin . 2016 . Dependent types and multi-monadic effects in F* . In Proc. POPL. 256 - 270 . Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella B\u00e9guelin. 2016. Dependent types and multi-monadic effects in F*. In Proc. POPL. 256-270.","journal-title":"Proc. POPL."},{"key":"e_1_3_2_2_41_1","first-page":"935","article-title":"Customizable Gradual Polymorphic Effects for Scala","author":"Toro Mat\u00edas","year":"2015","unstructured":"Mat\u00edas Toro and \u00c9ric Tanter . 2015 . Customizable Gradual Polymorphic Effects for Scala . In Proc. OOPSLA. 935 - 953 . Mat\u00edas Toro and \u00c9ric Tanter. 2015. Customizable Gradual Polymorphic Effects for Scala. In Proc. OOPSLA. 935-953.","journal-title":"Proc. OOPSLA."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314603","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314603","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314603","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314603"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":42,"alternative-id":["10.1145\/3314221.3314603","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314603","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}