Skip to Main content Skip to Navigation
New interface
Preprints, Working Papers, ...

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

Stéphane Fetcher 1 Luigi Liquori 2, 3 
1 SPI - Sémantiques, preuves et implantation
LIP6 - Laboratoire d'Informatique de Paris 6
2 MASCOTTE - Algorithms, simulation, combinatorics and optimization for telecommunications
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : 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.
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Luigi Liquori Connect in order to contact the contributor
Submitted on : Wednesday, May 13, 2015 - 12:45:15 PM
Last modification on : Thursday, August 4, 2022 - 4:52:44 PM
Long-term archiving on: : Wednesday, April 19, 2017 - 5:26:17 PM


Files produced by the author(s)


  • HAL Id : hal-01148949, version 1


Stéphane Fetcher, Luigi Liquori. Mini-Foc A Kernel Calculus for Certified Computer Algebra [Ongoing work]. 2005. ⟨hal-01148949⟩



Record views


Files downloads