Last week I worked on rmax. I spent most of the week formulating and proving different ways of representing the deletion of the largest node of a binary search tree. I have a few more ways I have to set up and prove. Also, the original case I was referring to (from the Coq official website) was not proved to completion, so I had to work on formulating that proof till the end. Stephanie will be out of town for the next two weeks, so I will be working a little more independently for the next few days. Three more weeks to go!

I also attended a graduate students' barbeque by Penn Engineering, a research talk by Andrew Tolmach, and a PhD dissertation defense over the week. All in all, I would say it was a very good week. I got free food, and listened to very smart people talk. : )

I spent the weekend in DC where I visited nearly 30 sights over the weekend. Needless to say, I slept in on Monday.

This week I hope to be done with rmax, and maybe look at some other algorithms. Also, I have been pulled away from Benjamin's class notes for a few days, so I need to restart my work in that area. Till next week, toodles!

July 14 - July 20