JSCert: Certified JavaScript

Table of Contents

Ignore this

no title here

RHSCupSmall.jpg

maintainer

webmaster:

body

Below is a list of publications which may be of interest to potential JSCert users and developers.

Peer Reviewed

A Trusted Mechanised JavaScript Specification (slides)
M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, G. Smith. Proc. of POPL '14. A quick tour of the Coq development can be found here.
Pretty-big-step-semantics-based Certified Abstract Interpretation
M. Bodin, T. Jensen, A. Schmitt. Proc. of JFLA '14.
Towards a Program Logic for JavaScript
P. Gardner, S. Maffeis, G. D. Smith. Proc. of POPL '12.
An Operational Semantics for Javascript
S. Maffeis, J.C. Mitchell and A. Taly. Proc. of APLAS '08.

Technical Reports

Towards a Program Logic for Javascript: Extended Techreport
P. Gardner, S. Maffeis, G. D. Smith.
JavaScript Small-Step Operational Semantics
S. Maffeis, J.C. Mitchell and A. Taly.

Related Work

ECMAScript
Our semantics are intended to closely follow the ECMA standards, for example ECMA-3 and ECMA 5.
Pretty-Big-Step Semantics
A. Charguéraud. ESOP '13.
Local Reasoning About Web Programs
G. D. Smith. PhD Thesis.
Local Reasoning about DOM
P. Gardner, G. D. Smith, M. J. Wheelhouse, U. D. Zarfaty. PODS '08.