Write a Blog >>
DLS 2018
Sun 4 - Fri 9 November 2018 Boston, Massachusetts, United States
co-located with SPLASH 2018
Tue 6 Nov 2018 11:00 - 11:30 at The Loft - Semantics Chair(s): Tim Felgentreff

The R programming language is very popular for developing statistical software and data analysis, thanks to rich libraries, concise and expressive syntax, and support for interactive programming. Yet, the semantics of R is fairly complex, contains many subtle corner cases, and is not formally specified. This makes it difficult to reason about R programs. In this work, we develop a big-step operational semantics for R in the form of an interpreter written in the Coq proof assistant. We ensure the trustworthiness of the formalization by introducing a monadic encoding that allows the Coq interpreter, CoqR, to be in direct visual correspondence with the reference R interpreter, GNU R. Additionally, we provide a testing framework that supports systematic comparison of CoqR and GNU R. In its current state, CoqR covers the nucleus of the R language as well as numerous additional features, making it pass a significant number of realistic test cases from the GNU R and FastR projects. To exercise the formal specification, we prove in Coq the preservation of memory invariants in selected parts of the interpreter. This work is an important first step towards a robust environment for formal verification of R programs.

Tue 6 Nov

dls-2018
10:30 - 12:00: DLS 2018 - Semantics at The Loft
Chair(s): Tim FelgentreffOracle Labs, Potsdam
dls-201810:30 - 11:00
Talk
Preston Tunnell WilsonBrown University, USA, Ben GreenmanNortheastern University, USA, Justin PombrioBrown University, USA, Shriram KrishnamurthiBrown University, USA
dls-201811:00 - 11:30
Talk
Martin BodinImperial College London, Tomás DiazUniversity of Chile, Chile, Éric TanterUniversity of Chile & Inria Paris