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
Prerequisites:
Experience in formalization in Isabelle, Familiarity with functional programming (e.g., ML, OCaml, Haskell, Lisp); English
Advisor:
Manuel Eberl, email {eberlm} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]