A New Formalization of Power Series in Coq

Abstract : To define elementary functions, proof assistants usually formalize power series. The Coq standard library is lacking with respect to the latter. This work presents a new formalization of power series. It is based on limits defined as total functions. My case study is Bessel functions.
Document type :
Conference papers
Complete list of metadatas

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/hal-00880212
Contributor : Catherine Lelay <>
Submitted on : Tuesday, November 5, 2013 - 3:49:26 PM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Friday, April 7, 2017 - 9:45:14 PM

File

article.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00880212, version 1

Collections

Citation

Catherine Lelay. A New Formalization of Power Series in Coq. The 5th Coq Workshop, Jul 2013, Rennes, France. ⟨hal-00880212⟩

Share

Metrics

Record views

250

Files downloads

201