The FoCaLiZe development environment
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
doc_src
focalizec
scratch
zvtov
.depend
.gitignore
AUTHORS
Announce
CHANGES
INSTALL
LICENSE
Makefile
Makefile.common
Makefile.rules
Makefile.utils
README
README_FOR_DEVELOPERS.html
TODO
configure
files-for-distrib.lst
opam

README

# ************************************************************************** #
#                                                                            #
#                        FoCaLiZe compiler                                   #
#                                                                            #
#            François Pessaux                                                #
#            Pierre Weis                                                     #
#            Damien Doligez                                                  #
#                                                                            #
#               LIP6  --  INRIA Rocquencourt -- ENSTA ParisTech              #
#                                                                            #
#  Copyright 2007 - 2012 LIP6 and INRIA                                      #
#            2012 ENSTA ParisTech                                            #
#  Distributed only by permission.                                           #
#                                                                            #
# ************************************************************************** #

The FoCaLiZe project attempts to provide a programming environment in which
one can design and develop certified programs.

The environment is based on a functional language with some object-oriented
features. That way, programmers can write the formal specifications and the
proofs of their code within the same setting. In FoCaLiZe, the proof
development is computer assisted via the Zenon proof finder; Zenon
dramatically leverage the amount of details to include in the proofs. In the
end, all the proofs are formally machine checked using the trusty Coq proof
checker.

Thanks to its inheritance and refinement mechanisms, FoCaLiZe encourages
incremental refinements of the specification until efficient executable code
is obtained (via a translation to Objective Caml).

As a real sized testbed, FoCaLiZe features a library for mathematical
structures, up to multivariate polynomial rings; this algebraic
infrastructure is equipped with complex algorithms that perform on par with
the best CAS in existence.