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
Re: RE: reference initialization
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2000-05-16 (02:07)
From: Patrick M Doane <patrick@w...>
Subject: Re: RE: reference initialization
On Mon, 15 May 2000 bdb-as-camluser@netcourrier.com wrote:

> Are there any languages in which the programmer can indicate proofs of
> safeness (regardless of fitness for a particular purpose) of the program
> he is writing, and let the compiler use these proofs? 

You might want to take a look at work by George Necula for Proof Carrying
Code (PCC), in particular his Touchstone compiler.

One of the optimizations performed by the compiler is the removal of
null-pointer checks. In cases where the compiler does not have enough
local information to remove the check, a precondition can be written that
will be used during optimization.

More about the compiler and PCC in general can be found at his website:


Patrick Doane