Following users demand, the validators are reactivated. The validator sources are available. The validator is written in Objective Caml. A Linux (i386) binary is also available.
The validator is to be installed in the place where you normaly put cgi-bin's (look at the Makefile). The validator has several fonctionalities, which are selected as follows.
validateis the name of the syntax validator,
compareis the name of the equivalence checker and
validate-fileis the name of both the syntax validator and the equivalence checker when the file upload feature is used.
The SML/NG validators are written using Jean-Christophe Filliatre
Thanks for your participation to this contest! In case you are curious, here are partial access statistics to the validator, sorted by number of accesses. Only accesses to the equivalence validator are recorded, some accesses were disregarded. As a matter of fact, we strongly suspect that we faced an attempt to overflow our server.
This page offers access to two experimental validators.
Validators may take their input directly, by accessing an url, or by uploading a file on your computer. The first method is recommended, since results are more detailled and that interaction is easier. The other two methods give control over the exact contents of your documents.
The size of your input is limited in all cases.
Your url must be given in normalized
Url's must be given in normalized