Dear Categories, Two papers about coinduction and guarded induction, one of them joint work with Martin Escardo, are available from http://www.cogs.susx.ac.uk/users/duskop/ or ftp://ftp.cogs.susx.ac.uk/pub/users/duskop/ *Calculus in coinductive form* is not one of those funny calculi where you can prove anything, just your old Newton-Leibniz-Taylor-Laplace calculus, with a special emphasis on Taylor and Laplace, and a bit of categories. *Guarded induction*, on the other hand, is this logical principle whereby, to prove a proposition p, you are allowed to use, among other things, that very same proposition p --- erm, provided, of course, that you make sure that it is #guarded#. This gives rise to various funny calculi, and a bit of categories. (Proper abstracts follow.) With best wishes, -- Dusko Pavlovic =================================================================== CALCULUS IN COINDUCTIVE FORM by D. Pavlovic and M.H. Escardo 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. =================================================================== GUARDED INDUCTION ON FINAL COALGEBRAS by D. Pavlovic Abstract. We make an initial step towards categorical semantics of guarded induction. While ordinary induction is usually modelled in terms of least fixpoints and initial algebras, guarded induction is based on *unique* fixpoints of certain operations, called guarded, on *final* coalgebras. So far, such operations were treated syntactically. We analyse them categorically. Guarded induction appears as couched in coinduction. The applications of the presented categorical analysis span across the gamut of the applications of coinduction, from modelling of computation to solving differential equations. A subsequent paper will provide an account of some domain theoretical aspects, which are presently left implicit.