Sat 13 Jan 2018 14:25 - 14:50 at Watercourt A - PL Metatheory Chair(s): Steve Zdancewic

Real-world programming languages have subtle behaviours. In particular, their semantics is often associated with various corner cases. Programmers are sometimes unaware of all these corner cases, which can yield to serious bugs. This is an opportunity for our community as Coq provides a way to certify the behaviour of a program. But if the certified program is not written in Coq, such a certification relies on a formal semantics of its programming language. In the case of a real-world language, such a semantics can be as difficult to trust as the original program. Some previous work proposed ways to trust such large semantics. This work evaluates the feasibility of such a large-scale formalisation in the case of the R programming languageā€”a trending programming language specialised in statistics. We introduce a formalisation of the core of R related to the reference R interpreter.

A Coq Formalisation of a Core of R (Bodin-CoqPL18.pdf)101KiB
Bodin-slides-CoqPL18.pdf (Bodin_coqpl18_slides.pdf)596KiB

Sat 13 Jan

CoqPL-2018
14:00 - 14:50: - PL Metatheory at Watercourt A
Chair(s): Steve Zdancewic
CoqPL-2018151584840000014:00 - 14:25
Talk
File Attached
CoqPL-2018151584990000014:25 - 14:50
Talk
File Attached