QArith: Coq Formalisation of Lazy Rational Arithmetic

Milad Niqui 1 Yves Bertot 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In this paper we present the formalisation of the library which is an implementation of rational numbers as binary sequences for both lazy and strict computation. We use the representation also known as the Stern-Brocot representation for rational numbers. This formalisation uses advanced machinery of the theorem prover and applies recent developments in formalising general recursive functions. This formalisation highlights the rôle of type theory both as a tool to verify hand-written programs and as a tool to generate verified programs.
Type de document :
[Research Report] RR-5004, INRIA. 2003, pp.19
Liste complète des métadonnées

Littérature citée [1 références]  Voir  Masquer  Télécharger
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 29 mai 2006 - 11:58:04
Dernière modification le : lundi 3 septembre 2018 - 10:56:01
Document(s) archivé(s) le : lundi 5 avril 2010 - 21:33:20



  • HAL Id : inria-00077041, version 1



Milad Niqui, Yves Bertot. QArith: Coq Formalisation of Lazy Rational Arithmetic. [Research Report] RR-5004, INRIA. 2003, pp.19. 〈inria-00077041〉



Consultations de la notice


Téléchargements de fichiers