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.
Isabelle/HOL, Standard ML
Experience in formalization in Isabelle, Familiarity with functional programming (e.g., ML, OCaml, Haskell, Lisp); English