Calcul de formules affines et de séries entières en arithmétique exacte avec types co-inductifs

Yves Bertot 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Nous décrivons une extension du travail de P. Di Gianantonio sur l'utilisation de types co-inductifs dans la description de librairies de calcul exact sur les nombres réels. Notre extension permet de représenter les séries formelles convergentes et de calculer sur ces représentations dans les systèmes de démonstration sur ordinateur qui disposent de réductions directes pour les fonctions structurelles récursives et les fonctions co-récursives gardées, comme le système Coq
Document type :
Conference papers
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000480
Contributor : Yves Bertot <>
Submitted on : Friday, October 21, 2005 - 5:28:48 PM
Last modification on : Monday, September 3, 2018 - 10:56:02 AM
Long-term archiving on: Thursday, April 1, 2010 - 10:53:06 PM

Identifiers

  • HAL Id : inria-00000480, version 1

Collections

Citation

Yves Bertot. Calcul de formules affines et de séries entières en arithmétique exacte avec types co-inductifs. Journées Francophones des Langages Applicatifs, INRIA, Jan 2006, Pauillac, pp.41-55. ⟨inria-00000480⟩

Share

Metrics

Record views

144

Files downloads

445