{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:26Z","timestamp":1772164046282,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Millenium Institute for Foundational Research on Data (IMFD Chile)."}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,10,24]]},"DOI":"10.1145\/3276945.3276946","type":"proceedings-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:28:39Z","timestamp":1540380519000},"page":"13-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A trustworthy mechanized formalization of R"],"prefix":"10.1145","author":[{"given":"Martin","family":"Bodin","sequence":"first","affiliation":[{"name":"University of Chile, Chile"}]},{"given":"Tom\u00e1s","family":"Diaz","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Karthikeyan Bhargavan Antoine Delignat-Lavaud and Sergio Maffeis. 2013. Language-Based Defenses Against Untrusted Browser Origins. In Usenix security symposium.   Karthikeyan Bhargavan Antoine Delignat-Lavaud and Sergio Maffeis. 2013. Language-Based Defenses Against Untrusted Browser Origins. In Usenix security symposium."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_3_2_1_3_1","unstructured":"Patrick Burns. 2011. The R Inferno.  Patrick Burns. 2011. The R Inferno."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3184558.3185969"},{"key":"e_1_3_2_1_5_1","unstructured":"ECMA International. 2010. Test262. https:\/\/github.com\/tc39\/test262 .  ECMA International. 2010. Test262. https:\/\/github.com\/tc39\/test262 ."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103663"},{"key":"e_1_3_2_1_7_1","unstructured":"Filippo Ghibellini. 2017. Dynamic test generation for R packages. Bachelor\u2019s Thesis.  Filippo Ghibellini. 2017. Dynamic test generation for R packages. Bachelor\u2019s Thesis."},{"key":"e_1_3_2_1_8_1","unstructured":"Google. {n. d.} R Style Guide. Retrieved 2018 from https:\/\/google. github.io\/styleguide\/Rguide.xml .  Google. {n. d.} R Style Guide. Retrieved 2018 from https:\/\/google. github.io\/styleguide\/Rguide.xml ."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Arjun Guha Claudiu Saftoiu and Shriram Krishnamurthi. 2010. The Essence of JavaScript. In ECOOP.   Arjun Guha Claudiu Saftoiu and Shriram Krishnamurthi. 2010. The Essence of JavaScript. In ECOOP.","DOI":"10.1007\/978-3-642-14107-2_7"},{"key":"e_1_3_2_1_10_1","article-title":"R: a Language for Data Analysis and Graphics","author":"Ihaka Ross","year":"1996","unstructured":"Ross Ihaka and Robert Gentleman . 1996 . R: a Language for Data Analysis and Graphics . Journal of computational and graphical statistics. Ross Ihaka and Robert Gentleman. 1996. R: a Language for Data Analysis and Graphics. Journal of computational and graphical statistics.","journal-title":"Journal of computational and graphical statistics."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2576195.2576205"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Robbert Krebbers and Freek Wiedijk. 2011. A Formalization of the C99 Standard in HOL Isabelle and Coq. In Calculemus\/mkm.   Robbert Krebbers and Freek Wiedijk. 2011. A Formalization of the C99 Standard in HOL Isabelle and Coq. In Calculemus\/mkm.","DOI":"10.1007\/978-3-642-22673-1_28"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_15_1","unstructured":"Xavier Leroy. 2014. How much is a mechanized proof worth certification-wise? In Principles in Practice.  Xavier Leroy. 2014. How much is a mechanized proof worth certification-wise? In Principles in Practice."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_22"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Sergio Maffeis John C. Mitchell and Ankur Taly. 2009. Isolating JavaScript with Filters Rewriting and Wrappers. In ESORICS.   Sergio Maffeis John C. Mitchell and Ankur Taly. 2009. Isolating JavaScript with Filters Rewriting and Wrappers. In ESORICS.","DOI":"10.1007\/978-3-642-04444-1_31"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.16"},{"key":"e_1_3_2_1_19_1","volume-title":"TestR: R Language Test Driven Specification. In The R User Conference, UseR!","author":"Maj Petr","year":"2013","unstructured":"Petr Maj , Tomas Kalibera , and Jan Vitek . 2013 . TestR: R Language Test Driven Specification. In The R User Conference, UseR! Petr Maj, Tomas Kalibera, and Jan Vitek. 2013. TestR: R Language Test Driven Specification. In The R User Conference, UseR!"},{"key":"e_1_3_2_1_20_1","volume-title":"Debugging in R. In The R User Conference, UseR!","author":"McPherson Jonathan","year":"2014","unstructured":"Jonathan McPherson . 2014 . Debugging in R. In The R User Conference, UseR! Jonathan McPherson. 2014. Debugging in R. In The R User Conference, UseR!"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Flor\u00e9al Morandat Brandon Hill Leo Osvald and Jan Vitek. 2012. Evaluating the design of the R language. In ECOOP.  Flor\u00e9al Morandat Brandon Hill Leo Osvald and Jan Vitek. 2012. Evaluating the design of the R language. In ECOOP.","DOI":"10.1007\/978-3-642-31057-7_6"},{"key":"e_1_3_2_1_22_1","unstructured":"Mozilla. 2013. Mozilla Automated JavaScript Tests. https:\/\/developer. mozilla . org \/ en - US \/ docs \/ SpiderMonkey \/ Running _ Automated _ JavaScript_Tests .  Mozilla. 2013. Mozilla Automated JavaScript Tests. https:\/\/developer. mozilla . org \/ en - US \/ docs \/ SpiderMonkey \/ Running _ Automated _ JavaScript_Tests ."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Joe Gibbs Politz Matthew J. Carroll Benjamin S. Lerner Justin Pombrio and Shriram Krishnamurthi. 2012. A Tested Semantics for Getters Setters and eval in JavaScript. DLS.  Joe Gibbs Politz Matthew J. Carroll Benjamin S. Lerner Justin Pombrio and Shriram Krishnamurthi. 2012. A Tested Semantics for Getters Setters and eval in JavaScript. DLS.","DOI":"10.1145\/2384577.2384579"},{"key":"e_1_3_2_1_25_1","volume-title":"R: A Language and Environment for Statistical Computing","author":"Team R Core","year":"2015","unstructured":"R Core Team . 2015 . R: A Language and Environment for Statistical Computing . R Foundation for Statistical Computing . https:\/\/www.R-project.org\/ . R Core Team. 2015. R: A Language and Environment for Statistical Computing. R Foundation for Statistical Computing. https:\/\/www.R-project.org\/ ."},{"key":"e_1_3_2_1_26_1","unstructured":"R Core Team. 2000. R Language Definition. R foundation for statistical computing.  R Core Team. 2000. R Language Definition. R foundation for statistical computing."},{"key":"e_1_3_2_1_27_1","unstructured":"R Core Team. {n. d.} The Comprehensive R Archive Network. Retrieved 2018 from https:\/\/cran.r-project.org\/ .  R Core Team. {n. d.} The Comprehensive R Archive Network. Retrieved 2018 from https:\/\/cran.r-project.org\/ ."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Gregor Richards Christian Hammer Brian Burg and Jan Vitek. 2011. The eval that Men Do. A large-scale study of the use of eval in javascript applications. In ECOOP.   Gregor Richards Christian Hammer Brian Burg and Jan Vitek. 2011. The eval that Men Do. A large-scale study of the use of eval in javascript applications. In ECOOP.","DOI":"10.1007\/978-3-642-22655-7_4"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.39"},{"key":"e_1_3_2_1_30_1","unstructured":"The Coq development team. 1984. the Coq Proof Assistant. Retrieved 2018 from https:\/\/coq.inria.fr\/ .  The Coq development team. 1984. the Coq Proof Assistant. Retrieved 2018 from https:\/\/coq.inria.fr\/ ."},{"key":"e_1_3_2_1_31_1","unstructured":"Luke Tierney Gabe Becker and Tomas Kalibera. 2017. ALTREP and Other Things. In R-devel.  Luke Tierney Gabe Becker and Tomas Kalibera. 2017. ALTREP and Other Things. In R-devel."},{"key":"e_1_3_2_1_32_1","volume-title":"TestR: Generating Unit Tests for R Internals. In The R User Conference, UseR!","author":"Tsegelskyi Roman","year":"2014","unstructured":"Roman Tsegelskyi and Jan Vitek . 2014 . TestR: Generating Unit Tests for R Internals. In The R User Conference, UseR! Roman Tsegelskyi and Jan Vitek. 2014. TestR: Generating Unit Tests for R Internals. In The R User Conference, UseR!"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Philip Wadler. 1992. Comprehending Monads. Mathematical structures in computer science.  Philip Wadler. 1992. Comprehending Monads. Mathematical structures in computer science.","DOI":"10.1017\/S0960129500001560"},{"key":"e_1_3_2_1_34_1","volume-title":"Truffle: A Self-Optimizing Runtime System.","author":"Wuerthinger Thomas","year":"2012","unstructured":"Thomas Wuerthinger . 2012 . Truffle: A Self-Optimizing Runtime System. Thomas Wuerthinger. 2012. Truffle: A Self-Optimizing Runtime System."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"event":{"name":"SPLASH '18: Conference on Systems, Programming, Languages, and Applications: Software for Humanity","location":"Boston MA USA","acronym":"SPLASH '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 14th ACM SIGPLAN International Symposium on Dynamic Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276945.3276946","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276945.3276946","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:57:41Z","timestamp":1750193861000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276945.3276946"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":35,"alternative-id":["10.1145\/3276945.3276946","10.1145\/3276945"],"URL":"https:\/\/doi.org\/10.1145\/3276945.3276946","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3393673.3276946","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}