JavaScript: de la standardisation à la formalisation

JavaScript est un langage complexe, mais dont la sémantique est très précisément définie. Il est donc envisageable de formellement prouver la correction d'un programme JavaScript étant donnée une formalisation de sa sémantique. Dans cet exposé, nous décrirons rapidement le langage, en insistant sur les aspects les plus surprenants. Nous motiverons le besoin d'une formalisation du langage dans un assistant de preuve et montrerons quelles formes elle peut prendre. Nous décrirons enfin les retombées de cette formalisation vis à vis du processus de standardisation, ainsi que ses différentes utilisations.

Alan Schmitt (INRIA)