[cwn] Attn: Development Editor, Latest Caml Weekly News

Alan Schmitt alan.schmitt at polytechnique.org
Tue May 11 01:04:50 PDT 2010


Hello,

Here is the latest Caml Weekly News, for the week of May 04 to 11, 2010.

1) New release of focalize, a development environment for high
integrity programs.
2) froc 0.2
3) Other Caml News

========================================================================
1) New release of focalize, a development environment for high
integrity programs.
------------------------------------------------------------------------
** Pierre Weis announced:

It is my pleasure to announce the new and second release for FoCaLiZe (the
0.6.0 FoCaLiZe opus).

Apart from updating the external tools (Caml, Camlp5 and Coq) this release
introduces inductive proofs on the representation of species. Zenon made
impressive progress so as to be helpful in proving inductive properties for
species.

Distributed with this version, we also have a nice tutorial for the language
and a set of additional examples.

The 0.6.0 release is available from FoCaLiZe.inria.fr at
<http://FoCaLiZe.inria.fr/download/focalize-0.6.0.tgz>

Uncompress, extract, then read the INSTALL file in the newly created
directory focalize.0.6.0 and follow the simple instructions written there.

To join people and discussions write to focalize-users at inria.fr.
Implementors also listen to suggestions and compliments at mail adress
focalize-devel at inria.fr.

Enjoy.

For the entire FoCaLiZe implementor group,

Pierre Weis.

Friday, May 7, 2010 10:36:44

What is it FoCaLiZe ?
---------------------

FoCaLiZe is an integrated development environment to write high integrity
programs and systems. It provides a purely functional language to formally
express specifications, describe the design and code the algorithms.
Within the functional language, FoCaLiZe provides a logical framework to
express the properties of the code. A simple declarative language provides
the natural expression of proofs of properties them from within the program
source code.

The FoCaLiZe compiler extracts statements and proof scripts from the source
file, to pass them to the Zenon proof generator to produce Coq proof terms
that are then formally verified.

The FoCaLiZe compiler also generates the code corresponding to the
program as an Objective Caml source file. This way, programs developped in
FoCaLiZe can be efficiently compiled to native code on a large variety of
architectures.

Last but not least, FoCaLiZe automatically generates the documentation
corresponding to the development, a requirement for high evaluation
assurance.

The FoCaLiZe system provides means for the developers to formally express
their specifications and to go step by step (in an incremental approach) to
design and implementation, while proving that their implementation
meets its specification or design requirements. The FoCaLiZe language offers
high level mechanisms such as inheritance, late binding, redefinition,
parametrization, etc. Confidence in proofs submitted by developers or
automatically generated ultimately relies on Coq formal proof verification.

FoCaLiZe is a son of the previous Focal system. However, it is a completely
new implementation with vastly revised syntax and semantices, featuring a
rock-solid infrastructure and greatly improved capabilities.
	
========================================================================
2) froc 0.2
Archive: <http://groups.google.com/group/fa.caml/browse_frm/thread/9af0a0bd98c11b09#>
------------------------------------------------------------------------
** Jake Donham announced:

I am happy to announce the release of version 0.2 of the froc library
for functional reactive programming in OCaml. There are a
number of improvements:

 * better event model: there is now a notion of simultaneous events,
and behaviors and events can now be freely mixed
 * self-adjusting computation (see
<http://ttic.uchicago.edu/~umut/projects/self-adjusting-computation/>)
is now supported via memo functions; needless recomputation can be
avoided in some cases
 * faster priority queue and timeline data structures
 * behavior and event types split into co- and contra-variant views
for subtyping
 * bug fixes and cleanup

Development of froc has moved from Google Code to Github; see

 * project page: <http://github.com/jaked/froc>
 * documentation: <http://jaked.github.com/froc>
 * downloads: <http://github.com/jaked/froc/downloads>

Thanks to Ruy Ley-Wild for helpful discussion, and to Daniel Bünzli
for helpful discussion and many good ideas in React.

You may be interested in this blog post describing the implementation:

 <http://ambassadortothecomputers.blogspot.com/2010/05/how-froc-works.html>

I hope you find this work useful. Let me know what you think.

========================================================================
3) Other Caml News
------------------------------------------------------------------------
** From the ocamlcore planet blog:

Thanks to Alp Mestan, we now include in the Caml Weekly News the links to the
recent posts from the ocamlcore planet blog at <http://planet.ocamlcore.org/>.

Uploaded sources of ocaml-semaphore to hg repository:
  <http://forge.ocamlcore.org/forum/forum.php?forum_id=604>

Make exploring large OCaml projects easy:
  <http://www.wisdomandwonder.com/link/4773/make-exploring-large-ocaml-projects-easy>

Use Amazon SimpleDB with OCaml:
  <http://www.wisdomandwonder.com/link/4769/use-amazon-simpledb-with-ocaml>

How froc works:
  <http://ambassadortothecomputers.blogspot.com/2010/05/how-froc-works.html>

ocaml-semaphore:
  <https://forge.ocamlcore.org/projects/ocaml-semaphore/>

Hardware failure and phishing attacks:
  <http://math.andrej.com/2010/05/04/hardware-failure-and-phishing-attacks/>

========================================================================
Old cwn
------------------------------------------------------------------------

If you happen to miss a CWN, you can send me a message
(alan.schmitt at polytechnique.org) and I'll mail it to you, or go take a look at
the archive (<http://alan.petitepomme.net/cwn/>) or the RSS feed of the
archives (<http://alan.petitepomme.net/cwn/cwn.rss>). If you also wish
to receive it every week by mail, you may subscribe online at
<http://lists.idyll.org/listinfo/caml-news-weekly/> .

========================================================================



More information about the caml-news-weekly mailing list