Abstract
Does the mechanization of semantics, as studied in the lecture on IMP and FUN mini-languages, scale up to real-world languages " " ? The third seminar addressed this question in the case of Javascript. After recalling the practical importance and great complexity of this language, the speaker described the JSCert project to mechanize the ECMAscript standard in Coq, including JSRef and JSExplain, executable forms of semantics that help to validate and understand it. With around 900 inductive rules, JSCert is reaching the limits of Coq's capacity. The speaker and his team are developing a particular form of operational semantics, the " skeletal " semantics, to better manage this complexity and make it easier to write abstract interpreters.
