The FoCaLiZe essential

Welcome to the FoCaLiZe website. This site offers information about FoCaLiZe, some documentation about the language and its compiler, some training opportunities, and of course, the latest release of FoCaLiZe.

Overview

The FoCaLiZe project aims at providing a programming environment to develop certified programs. The environment is based on a functional programming language with object-oriented features. The language allows the programmer to write formal specifications and proofs of the program in a unified and consistent setting.

From a FoCaLiZe source code development, the focalizec compiler produces three source files:

• a source file for the coq proof assistant to check the proofs,
• a source file for the ocaml compiler to build the executable program,
• a source file that contains the documentation extracted from the development sources.

Thanks to built-in inheritance mechanisms, the language allows to refine a development from the coarse-grain specification to the fully defined executable program.

The FoCaLiZe distribution includes a library of mathematical algebraic structures up to multivariate polynomial rings, a library of security policies and various examples contributed by FoCaLiZe users. The resulting libraries are noticeably efficent; for instance, the complex algorithms of the algebraic library provide runtime performances comparable to the best Computer Algebra Systems available.

New release of the FoCaLiZe environment soon

A new release of the FoCaLiZe environment, focalize 0.6.0, will be available in the coming days.

Current version of the FoCaLiZe environment

For about 3 years, the FoCaLiZe language and compiler have been rewritten from scratch. Numerous enhancements have been implemented. The syntax has been re-designed to be more homogenous and flexible. The core language provides new features like records, irrefutable pattern bindings, simpler "external" mappings... All syntactic elements (species, collection, record field, sum type constructors, ...) can be qualified. Entity parameters ("in" species parameter) are now managed in a smoother way, collections get a clearer "implementation" status, preventing confusion between collections and species in the FoCaLiZe philosophy. The compilation speed has been enhanced. The global architecture of the compiler enables third party analyses to be grafted onto the compiler before code generation. A new backend for the C language is under development and should be available soon (provided license issues can be worked out). This is the first public release of this entirely revised system. Currently François Pessaux, in collaboration with Pierre Weis and Damien Doligez are in charge of this new version of the FoCaLiZe environment. If you want more information, please feel free to contact us.

SSURF ANR project

The SSURF (Safety and Security UndeR Focal) ANR project has started. This project consists in :

• Analyze and define the features required for an IDE in order to reach high levels of security.
• Define a generic framework in which many access control policies can be expressed.

Further information (in french) can be found here.