Résumé
La mécanisation des sémantiques, comme étudiée dans le cours sur les mini-langages IMP et FUN, passe-t-elle à l’échelle de langages « du monde réel » ? Le troisième séminaire a abordé cette question dans le cas du langage Javascript. Après avoir rappelé l’importance pratique et la grande complexité de ce langage, le conférencier a décrit le projet JSCert de mécanisation en Coq du standard ECMAscript, incluant JSRef et JSExplain, des formes exécutables de la sémantique qui aident à la valider et la comprendre. Avec environ 900 règles inductives, JSCert arrive aux limites de capacité de Coq. Le conférencier et son équipe développent une forme particulière de sémantique opérationnelle, les sémantiques « squelettiques », pour mieux gérer cette complexité et faciliter l’écriture d’interprètes abstraits.
