The Atelier Focal  
Home
Login
Bug tracking
Overview PDF Print E-mail
Sunday, 24 October 2004
The Focal project attempts to provide a programming environment in which certified programs can be developed. This environment is based on a language including functional and object-oriented features. Moreover, this language provides means for the programmers to write formal specifications and proofs of their code, and to have them verified by a proof checker.
Thanks to inheritance and refinement mechanisms, Focal allows to make several refinements of a specification until providing an efficient executable code (obtained via a translation to OCaml).

Focal provides a library which implements mathematical structures up to multivariate polynomial rings and includes complex algorithms with performances comparable to the best CAS in existence.




Last Updated ( Thursday, 18 November 2004 )
 
SPI © 2004-2008
Contact Webmaster
powered by Joomla designed by CM, with help of the TiTi Dev Team

UPMC INRIA CNAM CNRS
LIP6 CEDRIC