## 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.