Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
[Caml-list] First alpha release of the FoC library
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Damien Doligez <Damien.Doligez@i...>
Subject: [Caml-list] First alpha release of the FoC library

We are pleased to announce the first release of the FOC library,  for
symbolic computation over polynomials. This release also contains a
compiler to Ocaml and Coq source code.

FOC source files contain some declarations and definitions of
functions, some statements about these functions and proofs of these
statements. The main programming features are
multiple inheritance, late binding, high-level parametrisation and
encapsulation mechanisms.   See the tutorial and the reference manuals
for details (and some research papers on our web site). This release 
provides  tools to produce XML formats (Openmath, Omdoc) and some
other tools helping the developer.

The library contains  the  FoC sources for
polynomial arithmetic using various representations:

- a general description of commutative algebra basic structures.
- Implementation of arbitrary precision integers using Ocaml big_ints.
- Polynomials using distributed (sparse) and recursive representations.
- Univariate subresultants calculations.
- Univariate polynomial factorization over finite fields.

Other sources have not been tested enough and are not compiled by
default. They are included for completeness.

This very first version must be considered as an
alpha-version. Although  in principle  proofs are required by the
system, the distributed library contains very few completed
proofs. Developing nice tools to do proofs is our long term goal. 
However, the system checks, with the help of the Coq prover,
that using together inheritance, late binding, parametrization do not
lead to inconsistencies. And users can already  do proofs within Coq.

The release is available at:
< >
and < >

The documentation is available on-line:
< >

Should you have any problem with the release, send a mail to Remember that this is work in progress. All
bug reports are welcome and any help will be appreciated.

-- Damien Doligez for the FoC team.

To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: