Calcul de formules affines et de sériesentì eres en arithmétique exacte avec types co-inductifs, Thérèse Hardin et Journées francophones des langages applicatifs. INRIA, 2006. ,
A coinductive approach to real numbers, Types 1999 Workshop, pp.114-130, 1956. ,
Elementary Functions, Algorithms and implementation, 1997. ,
URL : https://hal.archives-ouvertes.fr/ensl-00000008
Computing with Real Numbers, Lecture Notes in Computer Science, vol.2395, pp.193-267, 2000. ,
DOI : 10.1007/3-540-45699-6_5
Interactive Theorem Proving and Program Development, Coq'Art :the Calculus of Inductive Constructions, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Codifying guarded definitions with recursive schemes, Types for proofs and Programs, pp.39-59, 1994. ,
DOI : 10.1007/3-540-60579-7_3
Signed-digit number representations for fast parallel arithmetic, IRE Transactions on Electronic Computers, vol.10, pp.389-400, 1961. ,
Ajouter des entiers machinè a coq, 2006. ,
A Computational Approach to Pocklington Certificates in Type Theory, FLOPS, pp.97-113, 2006. ,
DOI : 10.1007/11737414_8
An exact arithmetic package for ml ,