English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
A sound semantics for OCaml light
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-11-09 (12:20)
From: Scott Owens <Scott.Owens@c...>
Subject: A sound semantics for OCaml light
We are pleased to announce the public release of OCaml light, a  
formal semantics for a substantial, practical subset of the Objective  
Caml language. It is written in Ott, generating proof assistant  
definitions for HOL-4 and (in draft form) Coq and Isabelle/HOL. It  
comprises a small-step operational semantics and a syntactic, non- 
algorithmic type system. A type soundness theorem has been proved and  
mechanized using the HOL-4 proof assistant. To ensure that the  
operational semantics accurately models Objective Caml, an executable  
version of the semantics has been created (and proved equivalent in  
HOL to the original, relational version) and tested on a number of  
small test cases.

For more information please visit http://www.cl.cam.ac.uk/~so294/ocaml.

-Scott, Gilles, Peter, and Tom