Automatic Laurent Series Expansions

Chair for Logic and Verification

Master Thesis

Sufficiently nice complex-valued functions admit Laurent series expansions, which can be computed symbolically. This is an important feature in Computer Algebra Systems like Mathematica that can be used to e.g. compute limits and complex residues. In this Master’s thesis project, a procedure is developed that computes such Laurent series inside the proof assistant Isabelle/HOL to aid the user by automatically proving limits, residues, and reasoning about poles.

Programming language:
Isabelle/HOL, Standard ML

Experience in formalization in Isabelle, Familiarity with functional programming (e.g., ML, OCaml, Haskell, Lisp); English

Manuel Eberl, email {eberlm} AT []

Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT []