Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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: -- (:)
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

-Scott, Gilles, Peter, and Tom