Paper: Calculus in Coinductive Form (at LICS 1998)

Authors: Dusko Pavlovic Martín H. Escardó

Abstract

Coinduction is often seen as a way of implementing infinite objects. Since real numbers are typical infinite objects, it may not come as a surprise that calculus, when presented in a suitable way, is permeated by coinductive reasoning. What is surprising is that mathematical techniques, recently developed in the context of computer science, seem to be shedding a new light on some basic methods of calculus. We introduce a coinductive formalization of elementary calculus that can be used as a tool for symbolic computation, and geared towards computer algebra and theorem proving. So far, we have covered parts of ordinary differential and difference equations, Taylor series, Laplace transform and the basics of the operator calculus

BibTeX

  @InProceedings{PavlovicEscard-CalculusinCoinducti,
    author = 	 {Dusko Pavlovic and Martín H. Escardó},
    title = 	 {Calculus in Coinductive Form},
    booktitle =  {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)},
    year =	 {1998},
    month =	 {June}, 
    pages =      {408--417},
    location =   {Indianapolis, IN, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }