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

14:00 - 14:50: - PL Metatheory at Watercourt A
Chair(s): Steve ZdancewicUniversity of Pennsylvania
CoqPL-2018151584840000014:00 - 14:25
Stephanie WeirichUniversity of Pennsylvania, USA, Antoine VoizardUniversity of Pennsylvannia, Anastasiya Kravchuk-Kirilyuk University of Pennsylvania
File Attached
CoqPL-2018151584990000014:25 - 14:50
File Attached