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 , 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.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger
Contributeur : Luigi Liquori <>
Soumis le : mercredi 13 mai 2015 - 12:45:15
Dernière modification le : mercredi 4 avril 2018 - 15:44:25
Document(s) archivé(s) le : mercredi 19 avril 2017 - 17:26:17


Fichiers produits par l'(les) auteur(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〉



Consultations de la notice


Téléchargements de fichiers