![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Tuesday 24 February 2009, 13:00-14:00
Formal power series in Isabelle/HOL
- đ¤ Speaker: Amine Chaieb (University of Cambridge)
- đ Date & Time: Tuesday 24 February 2009, 13:00 - 14:00
- đ Venue: Computer Laboratory, William Gates Building, Room SS03
Abstract
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.
Series This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- 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
- Martin's interesting talks
- School of Technology
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.