{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T04:17:04Z","timestamp":1748405824559,"version":"3.41.0"},"publisher-location":"Singapore","reference-count":27,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819789429"},{"type":"electronic","value":"9789819789436"}],"license":[{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-981-97-8943-6_14","type":"book-chapter","created":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T08:45:29Z","timestamp":1730105129000},"page":"283-302","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["OBRA: Oracle-Based, Relational, Algorithmic Type Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5983-3347","authenticated-orcid":false,"given":"Elizaveta","family":"Vasilenko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0732-5476","authenticated-orcid":false,"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,28]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Cardelli, L., Curien, P.: Formal parametric polymorphism. In: POPL (1993). https:\/\/doi.org\/10.1145\/158511.158622","DOI":"10.1145\/158511.158622"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Aguirre, A., Barthe, G., Birkedal, L., Bizjak, A., Gaboardi, M., Garg, D.: Relational reasoning for markov chains in a probabilistic guarded lambda calculus. In: ESOP (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_8","DOI":"10.1007\/978-3-319-89884-1_8"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Katsumata, S., Sato, T.: Higher-order probabilistic adversarial computations: categorical semantics and program logics. In: ICFP (2021).https:\/\/doi.org\/10.1145\/3473598","DOI":"10.1145\/3473598"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.: A relational logic for higher-order programs. In: ICFP (2017). https:\/\/doi.org\/10.1145\/3110265","DOI":"10.1145\/3110265"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"de Amorim, A.A., Arias, E.J.G., Gaboardi, M., Hsu, J.: Really natural linear indexed type checking. In: Implementation and Application of Functional Languages (2014). https:\/\/dl.acm.org\/doi\/10.1145\/2746325.2746335","DOI":"10.1145\/2746325.2746335"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Barthe, G., Fournet, C., Gr\u00e9goire, B., Strub, P., Swamy, N., B\u00e9guelin, S.Z.: Probabilistic relational verification for cryptographic implementations. In: POPL (2014). https:\/\/doi.org\/10.1145\/2535838.2535847","DOI":"10.1145\/2535838.2535847"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gaboardi, M., Arias, E.J.G., Hsu, J., Roth, A., Strub, P.: Higher-order approximate relational refinement types for mechanism design and differential privacy. In: POPL (2015). https:\/\/doi.org\/10.1145\/2676726.2677000","DOI":"10.1145\/2676726.2677000"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Coupling proofs are probabilistic product programs. In: POPL (2017). https:\/\/doi.org\/10.1145\/3093333.3009896","DOI":"10.1145\/3093333.3009896"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"\u00c7i\u00e7ek, E., Barthe, G., Gaboardi, M., Garg, D., Hoffmann, J.: Relational cost analysis. In: POPL (2017)","DOI":"10.1145\/3009837.3009858"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"\u00c7i\u00e7ek, E., Qu, W., Barthe, G., Gaboardi, M., Garg, D.: Bidirectional type checking for relational properties. In: PLDI (2019). https:\/\/doi.org\/10.1145\/3314221.3314603","DOI":"10.1145\/3314221.3314603"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Dunfield, J., Krishnaswami, N.: Bidirectional typing. ACM Comput. Surv. (2021). https:\/\/doi.org\/10.1145\/3450952","DOI":"10.1145\/3450952"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. In: POPL (2013). https:\/\/doi.org\/10.1145\/2429069.2429113","DOI":"10.1145\/2429069.2429113"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Grimm, N., Maillard, K., Fournet, C., Hritcu, C., Maffei, M., Protzenko, J., Ramananandro, T., Rastogi, A., Swamy, N., B\u00e9guelin, S.Z.: A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. In: CPP (2018). https:\/\/doi.org\/10.1145\/3167090","DOI":"10.1145\/3167090"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Handley, M.A.T., Vazou, N., Hutton, G.: Liquidate your assets: reasoning about resource usage in liquid Haskell. In: POPL (2019). https:\/\/doi.org\/10.1145\/3371092","DOI":"10.1145\/3371092"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Heintze, N., Riecke, J.G.: The SLam calculus: programming with secrecy and integrity. In: POPL (1998). http:\/\/doi.acm.org\/10.1145\/268946.268976","DOI":"10.1145\/268946.268976"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Jhala, R., Vazou, N.: Refinement types: a tutorial. In: Foundations and Trends in Programming Languages (2020). https:\/\/doi.org\/10.1561\/2500000032","DOI":"10.1561\/2500000032"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Nanevski, A., Banerjee, A., Garg, D.: Verification of information flow and access control policies with dependent types. In: S &P (2011). https:\/\/doi.org\/10.1109\/SP.2011.12","DOI":"10.1109\/SP.2011.12"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Banerjee, A., Garg, D.: Dependent type theory for verification of information flow and access control policies. In: TOPLAS (2013). http:\/\/doi.acm.org\/10.1145\/2491522.2491523","DOI":"10.1145\/2491522.2491523"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ML. In: POPL (2002). http:\/\/doi.acm.org\/10.1145\/503272.503302","DOI":"10.1145\/503272.503302"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Radicek, I., Barthe, G., Gaboardi, M., Garg, D., Zuleger, F.: Monadic refinements for relational cost analysis. In: POPL (2018). http:\/\/doi.acm.org\/10.1145\/3158124","DOI":"10.1145\/3158124"},{"key":"14_CR21","doi-asserted-by":"publisher","unstructured":"Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: ICFP (2010). https:\/\/doi.org\/10.1145\/1863543.1863568","DOI":"10.1145\/1863543.1863568"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Swamy, N., Hritcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P., Kohlweiss, M., Zinzindohoue, J.K., B\u00e9guelin, S.Z.: Dependent types and multi-monadic effects in F. In: POPL (2016). http:\/\/doi.acm.org\/10.1145\/2837614.2837655","DOI":"10.1145\/2837614.2837655"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Vasilenko, E., Vazou, N., Barthe, G.: Safe couplings: coupled refinement types. In: ICFP (2022). https:\/\/doi.org\/10.1145\/3547643","DOI":"10.1145\/3547643"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Vazou, N., Breitner, J., Kunkel, R., Van\u00a0Horn, D., Hutton, G.: Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). In: Haskell (2018). https:\/\/doi.org\/10.1145\/3242744.3242756","DOI":"10.1145\/3242744.3242756"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for Haskell. In: ICFP (2014). https:\/\/doi.org\/10.1145\/2692915.2628161","DOI":"10.1145\/2692915.2628161"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Vazou, N., Tondwalkar, A., Choudhury, V., Scott, R.G., Newton, R.R., Wadler, P., Jhala, R.: Refinement reflection: complete verification with SMT. In: POPL (2017). https:\/\/doi.org\/10.1145\/3158141","DOI":"10.1145\/3158141"},{"key":"14_CR27","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Propositions as types. Commun. ACM (2015). https:\/\/doi.org\/10.1145\/2699407","DOI":"10.1145\/2699407"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-97-8943-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T16:52:41Z","timestamp":1748364761000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-97-8943-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,28]]},"ISBN":["9789819789429","9789819789436"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-981-97-8943-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,28]]},"assertion":[{"value":"28 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}