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