Interdisciplinary Project (IDP)
Line integrals are a basic concept of integration that evolved in the context of physics, but currently has many applications [1,2]. An Isabelle/HOL theory of line integrals was developed as a part of formalising Green’s theorem [3]. In this project the student would work on extending the existing theory of line integrals by proving more of their properties, with a special focus on practically useful properties of them, like evaluation of different line integrals. A second possibility is developing a theory of surface integrals, which could be seen as a generalisation of the existing theory of line integrals. Useful resources on line integrals and surface integrals are the following books:
- Peter R. Baxandall and Hans Liebeck. Vector calculus. Oxford University Press, USA, 1986.
- Michael Spivak. A comprehensive introduction to differential geometry, 1979.
- Vladimir Antonovich Zorich and Octavio Paniagua. Mathematical analysis II. Berlin: Springer, 2016.
Prerequisites:
Experience with Isabelle/HOL is required.
Advisor:
Mohammad Abdulaziz, email {mansour} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]
Material to read:
[1]
Rachel A. Kuske and Joseph B. Keller. Optimal exercise boundary for an American put option. Applied Mathematical Finance 5.2 (1998): 107-116.
[2]
J. D. Evans and R. Kuske, and Joseph B. Keller. American options on assets with dividends near expiry. Mathematical Finance 12.3 (2002): 219-237.
[3]
Mohammad Abdulaziz and Lawrence C. Paulson. An Isabelle/HOL formalisation of Green’s theorem. Journal of Automated Reasoning 63.3 (2019): 763-786.