BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formal power series in Isabelle/HOL - Amine Chaieb (University of 
 Cambridge)
DTSTART:20090224T130000Z
DTEND:20090224T140000Z
UID:TALK16357@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:We show how to use (axiomatic) type classes to formalize \nfor
 mal power series (FPS) over arbitrary domains. We prove that if the basic 
 domain is an integral domain\, the so is the FPS construction. We also for
 malize multiplicative inverses and division\, arbitrary nth \nroots\, comp
 osition of FPS and the compositional inverses. We present simple proofs an
 d formalizations from Generatingfunctionology by Wilf and formalize some e
 lementary FPS like the exponential\, logarithmic\, \nbinomial\, and some t
 rigonometric series and some of their simple applications. From this forma
 lization we immediately obtain (for free) the field of formal Laurent seri
 es and with minimal efforts a formalization of polynomials. All formalizat
 ions referred to above are univariate.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR