April 2006
March 2006
The HEVEA Home page
by GeorgesMariano
HEVEA is a quite complete and fast LATEX to HTML translator. HEVEA is written in Objective Caml. HEVEA now renders symbols by using the so-called HTML “entites”. Modern browsers display those entities correctly most of the time. By contrast, previo
February 2006
January 2006
Menhir
by GeorgesMariano
Menhir est un générateur d'analyseurs syntaxiques LR(1) pour le langage de programmation Objective Caml. En d'autres termes, Menhir traduit des spécifications de grammaires LR(1) en code Objective Caml. Menhir a été conçu et implémenté par Franço
CDuce: Home page
by GeorgesMariano & 1 other
CDuce is a modern XML-oriented functional language with innovative features. A compiler is available under the terms of an open-source license. CDuce is type-safe, efficient, and offer powerful constructions to work with XML documents.
The Compcert certified compiler back-end
by GeorgesMariano
The Compcert back-end is a compiler that generates PowerPC assembly code from a low-level intermediate language called Cminor and a slightly more expressive intermediate language called Csharpminor. The particularity of this compiler is that it is written
Why: a software verification tool
by GeorgesMariano
Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for
1
(15 marks)
