Mini-Foc A Kernel Calculus for Certified Computer Algebra [Ongoing work]

The Foc language is designed to bring solutions on the reliability of the software, in particular on the development and the reusing of certified libraries, especially for Certified Computer Algebra. The Foc project aims at building an environment to develop certified computer algebra libraries. The project develops a language called Foc, where any implementation must come with a proof of its correctness. This includes of course pre- and post- condition statements, but also proofs of purely mathematical theorems. In this context, reusability of the code, but also of the correctness proofs is of very important concern: a tool written for mathematical Groups should be available for the mathematical Rings, provided the system knows that every Ring is a Group, wich can be faithfully modeled by suitable subtyping relation. For this, this formal language allows to implement certified components called Collections. These collections are specified and implemented step by step: the programmer describes formally – the properties of the algorithm, – the context in which they are executed, – the data representation and proves formally that the implemented algorithms satisfies the specified properties. This programming paradigm implies the use of classic oriented-object features and the use of module features like interfaces and encapsulation of data representation. This conception of the object oriented programming brings the question where the Foc language is situated in relation to others more classic object-oriented languages. To answer to this question, we propose a kernel of Foc called Mini-Foc. With this kernel, we are interested by the programming aspect of Foc (proof aspect are left to suitable extensions). Thus, the main ingredients of Mini-Foc, are multiple inheritance, late binding, overriding, interfaces and encapsulation of the data representation. We specify formally the syntax, the semantics and the type system