From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 05E9F5D4 for ; Mon, 3 Sep 2018 08:38:31 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.53,324,1531778400"; d="scan'208,217";a="344640785" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 03 Sep 2018 10:38:29 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 5DB87824DC; Mon, 3 Sep 2018 10:38:29 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id EA90E824DB for ; Mon, 3 Sep 2018 10:38:21 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=francois.pessaux@ensta-paristech.fr; spf=Pass smtp.mailfrom=francois.pessaux@ensta-paristech.fr; spf=Pass smtp.helo=postmaster@ns3.ensta.fr IronPort-PHdr: =?us-ascii?q?9a23=3AwymQXRBnw5ppYQFgYYTCUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPT/osbcNUDSrc9gkEXOFd2Cra4c1KyO6+jJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fcbglUhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfO?= =?us-ascii?q?pWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnM?= =?us-ascii?q?VhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykC?= =?us-ascii?q?oJNyI2/27KhMJ+gqJVvhCuqR94zYPPeo6ZKP9+c7ndfd8GR2dMWNtaWSxbAoO7?= =?us-ascii?q?aosCF+oPPfxCoIn7v1wOqhq+BRK0C+311DBInWT20rcn0+UuDArL2wIgH8gUv3?= =?us-ascii?q?TSsNr1M6YSUfuvwKnQ0zrDdOhW1i3g6InHaR0uv/eMXalsccXL0EUvDxnKjk+R?= =?us-ascii?q?qYz+IzOayPgCs2iB4+puT+KikmgqoBx/rDiow8cjkIjJhoQNx1DF8yV52oc1Ks?= =?us-ascii?q?eiRE51e96oCJRQtyCGN4t2X8MtWHtktzo9yr0Dv5OwYSsEyIw/yhLCZPGKcZKE?= =?us-ascii?q?7gzjWeqNOzt0mW5pdKixihqq7EStxe/xWtOq3FtKsiZJiMfAum4D2hDJ5MWLVv?= =?us-ascii?q?1w9Vq71zmVzQDc8ORELFg0laXFL54hxaY9lpwIsUnNBCP5hkP2jLSKdko+4OSo?= =?us-ascii?q?5f7nbq3npp+aKYB0lhnzPrkhl8G9G+g0LAgDU3SB9eihyLHv50P0TK1PjvIsk6?= =?us-ascii?q?nZtJ7aJd4cpq68GwJV3Jwj5Ay5Dzi619QYnGIHIEhdeB2ZlIjpIEvBIO33DPqk?= =?us-ascii?q?nVuslixrx+zcMbH4GpXCNGLDkLb6fbZh9UFT1AozwcpR55JOEr0BOu78WlfttN?= =?us-ascii?q?zECR80KxC7zPziCNV5z48eXWOPArSFMK7Jql+J5ucvI/GWa4MPuTb9LeIl5//0?= =?us-ascii?q?gnMjl18dZ/rh4ZxCY3m9GrFiIl6FSXvqmNYIV2kQ7SQkS+m/pkeLV7FUZm2FZ6?= =?us-ascii?q?8n/TgmGMryA53KQIuqgafHxCqgBZRLdkhLDEuQGDLwfp+FQOsBYyLULNU3wW9M?= =?us-ascii?q?bqSoV4J0jULmjwT90bcydrOFqB1djorq0Z1O38OWkBgz8TJuCMHHizOASXpoly?= =?us-ascii?q?YQTiU3x7xyqkw7xE3RiPEk0cwdLsRa4rZyail/LYTVlbQoBtbpRguEZt6TSU26?= =?us-ascii?q?T96mRz8rHIpono0+Jn1lEtDntSjtmiqnB7hMy+6NH8dy/6THw3G3Kdwvkns=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BVAgCC8YxbhwMK+pNaHQEBBQELAYQzf?= =?us-ascii?q?yiDcohwi0yBaI1/gxWHOC6ESQKDQBoGAQQ0FAECAQECAQEBAQETAQEBCgsJCCk?= =?us-ascii?q?jDII1IoJhAwMjZkoDAgJGERmDIQGCAQUKoUYRgSKBLog2gUWCLYgrgheBOQwTh?= =?us-ascii?q?WcCgUEBAYMfMYImAogbilyIXwcCf4U1gSmIHBeBQEiGRiWFZoowd4VehAMOJ4F?= =?us-ascii?q?2TSd2AYJBCTWBdYNOgT6JFm0BAQGMI4I7AQE?= X-IPAS-Result: =?us-ascii?q?A0BVAgCC8YxbhwMK+pNaHQEBBQELAYQzfyiDcohwi0yBaI1?= =?us-ascii?q?/gxWHOC6ESQKDQBoGAQQ0FAECAQECAQEBAQETAQEBCgsJCCkjDII1IoJhAwMjZ?= =?us-ascii?q?koDAgJGERmDIQGCAQUKoUYRgSKBLog2gUWCLYgrgheBOQwThWcCgUEBAYMfMYI?= =?us-ascii?q?mAogbilyIXwcCf4U1gSmIHBeBQEiGRiWFZoowd4VehAMOJ4F2TSd2AYJBCTWBd?= =?us-ascii?q?YNOgT6JFm0BAQGMI4I7AQE?= X-IronPort-AV: E=Sophos;i="5.53,324,1531778400"; d="scan'208,217";a="277515619" Received: from ns3.ensta.fr ([147.250.10.3]) by mail3-smtp-sop.national.inria.fr with ESMTP; 03 Sep 2018 10:38:20 +0200 Received: from ns3.ensta.fr (localhost [127.0.0.1]) by ns3.ensta.fr (Postfix) with ESMTP id D896B13184B for ; Mon, 3 Sep 2018 10:38:18 +0200 (CEST) X-Virus-Scanned: amavisd-new at ns3.ensta.fr Received: from ns3.ensta.fr ([127.0.0.1]) by ns3.ensta.fr (ns3.ensta.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id milJ62Lqz22n for ; Mon, 3 Sep 2018 10:38:16 +0200 (CEST) Received: from zemail2.ensta.fr (zemail.ensta.fr [147.250.1.15]) by ns3.ensta.fr (Postfix) with ESMTP id 9A0B0131847 for ; Mon, 3 Sep 2018 10:38:16 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail2.ensta.fr (Postfix) with ESMTP id 923D03C08C7 for ; Mon, 3 Sep 2018 10:38:16 +0200 (CEST) Received: from zemail2.ensta.fr ([127.0.0.1]) by localhost (zemail2.ensta.fr [127.0.0.1]) (amavisd-new, port 10032) with ESMTP id lh9F3UR6D4kt for ; Mon, 3 Sep 2018 10:38:15 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail2.ensta.fr (Postfix) with ESMTP id DFCF53C0931 for ; Mon, 3 Sep 2018 10:38:15 +0200 (CEST) X-Virus-Scanned: amavisd-new at zemail2.ensta.fr Received: from zemail2.ensta.fr ([127.0.0.1]) by localhost (zemail2.ensta.fr [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id 8U_6DCRXBZ8n for ; Mon, 3 Sep 2018 10:38:15 +0200 (CEST) Received: from [147.250.223.30] (unknown [147.250.223.30]) by zemail2.ensta.fr (Postfix) with ESMTPSA id BC1BF3C08C7 for ; Mon, 3 Sep 2018 10:38:15 +0200 (CEST) From: =?utf-8?Q?Fran=C3=A7ois_Pessaux?= Content-Type: multipart/alternative; boundary="Apple-Mail=_ACDC084B-84B9-4541-8946-B27E99D9F4F1" Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.1\)) Date: Mon, 3 Sep 2018 10:38:15 +0200 References: To: caml-list@inria.fr In-Reply-To: Message-Id: <1C15EE94-097B-4758-815F-1F9D0BB5EF6C@ensta.fr> X-Mailer: Apple Mail (2.3445.9.1) Subject: [Caml-list] FoCaLiZe 0.9.2 released Reply-To: =?utf-8?Q?Fran=C3=A7ois_Pessaux?= X-Loop: caml-list@inria.fr X-Sequence: 17041 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --Apple-Mail=_ACDC084B-84B9-4541-8946-B27E99D9F4F1 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 It is my pleasure to announce the new release for FoCaLiZe (the 0.9.2 versi= on). As for previous releases, some bugs have been fixed in the focalizec compil= er.=20 This version introduces the Dedukti backend written by Rapha=C3=ABl Cauderl= ier, taking benefits from Zenon_modulo to ease proofs.=20 The Coq backend now generates Coq code compatible with Coq 8.8. A complete = description of changes / new features can in found in the CHANGES file of t= he distribution. A complete description of changes / new features can in found in the CHANGES file of the distribution. The 0.9.2 release is available from focalize.inria.fr at http://focalize.inria.fr/download/focalize-0.9.2.tgz Uncompress, extract, then read the INSTALL file in the newly created directory focalize.0.9.2 and follow the simple instructions written there. A public GIT repository is also available on GitHub (https://github.com/pes= saux-f/focalize ), allowing to fetch the latest development state of FoCaLiZe. However, its co= ntent is not bullet-proof and may be unstable at some times. It reflects the real= -time state of FoCaLiZe and may bring fixes and features not available in previous releases and that will be part of the next release. To join people and discussions write to focalize-users@inria.fr . Implementors also listen to suggestions (and compliments if some ^_^) at the mail address: focalize-devel@inria.fr . Enjoy. For the entire FoCaLiZe implementation group, Fran=C3=A7ois Pessaux. September 2018 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 developed 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 semantics, featuring a rock-solid infrastructure and greatly improved capabilities. --=20 Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs= --Apple-Mail=_ACDC084B-84B9-4541-8946-B27E99D9F4F1 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 It is my pleasure to announce the new release for FoCaLiZe (the 0.9.2= version).
As for previous releases, some b=
ugs have been fixed in the focalizec compiler. 
This version introduces the Dedukti backend writ=
ten by Rapha=C3=ABl Cauderlier, taking benefits from Zenon_modulo to ease pro=
ofs. 
The Coq backe=
nd now generates Coq code compatible with Coq 8.8. A complete description of ch=
anges / new features can in found in the CHANGES file of the distribution.<=
/span>
A complete description of changes / new features can in found in the CHANGES
file of the distribution.

The 0.9.2 release is available from focalize.inria.fr at
http://focalize.inria.fr/download/focalize-0.9.2.tgz
Uncompress, extract, then read the INSTALL file in the newly created
directory focalize.0.9.2 and follow the simple instructions written there.


A public GIT repository is also available on GitHub (https://github.com/pessaux-f/focaliz=
e),
allowing to fetch the latest development state of FoCaLiZe. However, its co=
ntent
is not bullet-proof and may be unstable at some times. It reflects the real=
-time
state of FoCaLiZe and may bring fixes and features not available in previous
releases and that will be part of the next release.
To=
 join people and discussions write to focalize-users@inria.fr.
Implementors also listen to suggestions (and compliments if some ^_^) at the
mail address: focaliz=
e-devel@inria.fr.

Enjoy.

For the entire FoCaLiZe implementation group,

Fran=C3=A7ois Pessaux.

September 2018

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 developed 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 semantics, featuring a
rock-solid infrastructure and greatly improved capabilities.


= --Apple-Mail=_ACDC084B-84B9-4541-8946-B27E99D9F4F1--