Formal power series in Isabelle/HOL

Add to your list(s) Download to your calendar using vCal

• Amine Chaieb (University of Cambridge)
• Tuesday 24 February 2009, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

We show how to use (axiomatic) type classes to formalize formal 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 formalize multiplicative inverses and division, arbitrary nth roots, composition of FPS and the compositional inverses. We present simple proofs and formalizations from Generatingfunctionology by Wilf and formalize some elementary FPS like the exponential, logarithmic, binomial, and some trigonometric series and some of their simple applications. From this formalization we immediately obtain (for free) the field of formal Laurent series and with minimal efforts a formalization of polynomials. All formalizations referred to above are univariate.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.