# Joint talk with Bath University: Landau in Agda

## Yoshiki Kinoshita

(AIST Japan)

I am writing proofs to the propositions in Landau's Grundlagen der Analysis (Foundation of Analysis). Although the work is still at an early stage (only completed the addition of natural numbers), I have some observations comparing Landau's original proofs and proofs suitable for Agda. I will talk about those observations, as well as a

small tool which represents equational and inequational proofs nicely.

**Thursday 22nd October 2009, 14:00**

Far-134 (Access grid room)

Department of Computer Science