{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T07:37:34Z","timestamp":1775029054060,"version":"3.50.1"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319737201","type":"print"},{"value":"9783319737218","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-73721-8_13","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T04:13:05Z","timestamp":1514434385000},"page":"269-290","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Refinement Types for Ruby"],"prefix":"10.1007","author":[{"given":"Milod","family":"Kazerounian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Austin","family":"Bourgerie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeffrey S.","family":"Foster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"key":"13_CR1","unstructured":"Aggregate (2017). https:\/\/github.com\/josephruscio\/aggregate"},{"key":"13_CR2","unstructured":"Boxroom (2017). https:\/\/github.com\/mischa78\/boxroom"},{"key":"13_CR3","unstructured":"Businesstime (2017). https:\/\/github.com\/bokmann\/business_time\/"},{"key":"13_CR4","unstructured":"Geokit (2017). https:\/\/github.com\/geokit\/geokit"},{"key":"13_CR5","unstructured":"Matrix (2017). https:\/\/github.com\/ruby\/matrix"},{"key":"13_CR6","unstructured":"Money (2017). https:\/\/github.com\/RubyMoney\/money"},{"key":"13_CR7","unstructured":"Unitwise (2017). https:\/\/github.com\/joshwlewis\/unitwise\/"},{"key":"13_CR8","unstructured":"Verified ruby apps (2017). https:\/\/raw.githubusercontent.com\/mckaz\/milod.kazerounian.github.io\/master\/static\/VMCAI18\/source.md"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.Y.: A relational logic for higher-order programs (2017)","DOI":"10.1145\/3110265"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Ancona, D., Ancona, M., Cuni, A., Matsakis, N.D.: Rpython: A step towards reconciling dynamically and statically typed oo languages. In: DLS (2007)","DOI":"10.1145\/1297081.1297091"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/11531142_19","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"C Anderson","year":"2005","unstructured":"Anderson, C., Giannini, P., Drossopoulou, S.: Towards type inference for JavaScript. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 428\u2013452. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11531142_19"},{"key":"13_CR12","unstructured":"Aycock, J.: Aggressive type inference. In: International Python Conference (2000)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-662-44202-9_11","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"G Bierman","year":"2014","unstructured":"Bierman, G., Abadi, M., Torgersen, M.: Understanding TypeScript. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 257\u2013281. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_11"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Boci\u0107, I., Bultan, T.: Symbolic model extraction for web application verification. In: ICSE (2017)","DOI":"10.1109\/ICSE.2017.72"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Chaudhuri, A., Foster, J.S.: Symbolic security analysis of ruby-on-rails web applications. In: CCS (2010)","DOI":"10.1145\/1866307.1866373"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/3-540-49538-X_5","volume-title":"ECOOP\u201995 \u2014 Object-Oriented Programming, 9th European Conference, \u00c5arhus, Denmark, August 7\u201311, 1995","author":"J Dean","year":"1995","unstructured":"Dean, J., Grove, D., Chambers, C.: Optimization of Object-Oriented Programs using static class hierarchy analysis. In: Tokoro, M., Pareschi, R. (eds.) ECOOP 1995. LNCS, vol. 952, pp. 77\u2013101. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-49538-X_5"},{"key":"13_CR17","unstructured":"Foster, J., Ren, B., Strickland, S., Yu, A., Kazerounian, M.: RDL: Types, type checking, and contracts for Ruby (2017). https:\/\/github.com\/plum-umd\/rdl"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Freeman, T., Pfenning, F.: Refinement types for ML (1991)","DOI":"10.1145\/113445.113468"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Jeon, J., Qiu, X., Foster, J.S., Solar-Lezama, A.: Jsketch: Sketching for java. In: ESEC\/FSE 2015 (2015)","DOI":"10.1145\/2786805.2803189"},{"key":"13_CR20","unstructured":"Jones, C.: Specification and design of (parallel) programs. In: IFIP Congress (1983)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Kent, A.M., Kempe, D., Tobin-Hochstadt, S.: Occurrence typing modulo theories. In: PLDI (2016)","DOI":"10.1145\/2908080.2908091"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Lerner, B.S., Politz, J.G., Guha, A., Krishnamurthi, S.: Tejas: Retrofitting type systems for JavaScript (2013)","DOI":"10.1145\/2508168.2508170"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Near, J.P., Jackson, D.: Rubicon: Bounded verification of web applications. In: FSE 2012 (2012)","DOI":"10.1145\/2393596.2393667"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Near, J.P., Jackson, D.: Finding security bugs in web applications using a catalog of access control patterns. In: ICSE 2016 (2016)","DOI":"10.1145\/2884781.2884836"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-41540-6_2","volume-title":"Computer Aided Verification","author":"S Pernsteiner","year":"2016","unstructured":"Pernsteiner, S., Loncaric, C., Torlak, E., Tatlock, Z., Wang, X., Ernst, M.D., Jacky, J.: Investigating safety of a radiotherapy machine using system models with pluggable checkers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 23\u201341. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_2"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Protzenko, J., Zinzindohou\u00e9, J.K., Rastogi, A., Ramananandro, T., Wang, P., Zanella-B\u00e9guelin, S., Delignat-Lavaud, A., Hri\u0163cu, C., Bhargavan, K., Fournet, C., Swamy, N.: Verified low-level programming embedded in f* (2017)","DOI":"10.1145\/3110261"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Rastogi, A., Swamy, N., Fournet, C., Bierman, G., Vekris, P.: Safe & efficient gradual typing for TypeScript (2015)","DOI":"10.1145\/2676726.2676971"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Ren, B.M., Foster, J.S.: Just-in-time static type checking for dynamic languages. In: PLDI (2016)","DOI":"10.1145\/2908080.2908127"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: PLDI (2008)","DOI":"10.1145\/1375581.1375602"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in pvs. IEEE Trans. Softw., Eng. (1998)","DOI":"10.1109\/32.713327"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. In: LFP 1992 (1992)","DOI":"10.1145\/141471.141563"},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: PLDI (2013)","DOI":"10.1145\/2491956.2462195"},{"key":"13_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-540-31987-0_28","volume-title":"Programming Languages and Systems","author":"P Thiemann","year":"2005","unstructured":"Thiemann, P.: Towards a type system for analyzing JavaScript programs. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 408\u2013422. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_28"},{"key":"13_CR36","doi-asserted-by":"crossref","unstructured":"Tobin-Hochstadt, S., Felleisen, M.: Interlanguage migration: From scripts to programs. In: OOPSLA (2006)","DOI":"10.1145\/1176617.1176755"},{"key":"13_CR37","doi-asserted-by":"crossref","unstructured":"Tobin-Hochstadt, S., Felleisen, M.: The design and implementation of typed scheme. In: POPL (2008)","DOI":"10.1145\/1328438.1328486"},{"key":"13_CR38","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bodik, R.: Growing solver-aided languages with rosette. Onward! (2013)","DOI":"10.1145\/2509578.2509586"},{"key":"13_CR39","doi-asserted-by":"crossref","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for haskell (2014)","DOI":"10.1145\/2628136.2628161"},{"key":"13_CR40","doi-asserted-by":"crossref","unstructured":"Vekris, P., Cosman, B., Jhala, R.: Refinement types for TypeScript (2016)","DOI":"10.1145\/2908080.2908110"},{"key":"13_CR41","doi-asserted-by":"crossref","unstructured":"Vytiniotis, D., Peyton Jones, S., Claessen, K., Ros\u00e9n, D.: Halo: Haskell to logic through denotational semantics. In: POPL (2013)","DOI":"10.1145\/2429069.2429121"},{"key":"13_CR42","doi-asserted-by":"crossref","unstructured":"Weitz, K., Woos, D., Torlak, E., Ernst, M.D., Krishnamurthy, A., Tatlock, Z.: Scalable verification of border gateway protocol configurations with an SMT solver. In: OOPSLA (2016)","DOI":"10.1145\/2983990.2984012"},{"key":"13_CR43","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: PLDI (1998)","DOI":"10.1145\/277650.277732"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73721-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T16:01:10Z","timestamp":1570550470000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}