Entering Candidacy

Friday 19 August 2005 6:21 pm

I am now officially running for the office of PhD. In other words, I passed my A-exam. I’d say the presentation went quite well, as there were at least a few people who didn’t seem completely baffled by the work. A number of people even asked questions, which was the part I dreaded the most. However, they were all answerable questions and I’d like to think I held my own in responding. This means I now have my Masters degree and, as Dexter said, “all you have to do now is write a thesis.”

The Next PhD Step: A-Exam

Wednesday 17 August 2005 10:16 pm

On Friday, I will be presenting my A-Exam for admission to candidacy in the PhD program. The work is based on the paper I presented at MKM in Germany. Below is the announcement for my exam and any of you in Ithaca are more than welcome to attend!

Title: A Proof-Theoretic Approach to Hierarchical Math Library Organization
Speaker: Kamal Aboul-Hosn
When: Friday, 19 August 2005 at 11:00am
Location: Rhodes 484

The relationship between theorems and lemmas in mathematical reasoning is often vague. Nevertheless, the decisions we make in creating lemmas provide an inherent hierarchical structure to the statements we prove. Theorem provers generally have flat library structures with no formal distinction between lemmas and theorems. The reasons to distinguish lemmas from theorems in these systems is the same as the reasons in papers: to ascribe various levels of importance and to introduce dependency or scoping relationships. We seek to formalize these notions and provide a proof-theoretic means by which to organize a set of proofs in a hierarchical fashion that reflects this natural structure.

In this talk, we propose a system that represents and manipulates scope formally through the structure of the library of proofs. We provide a representation of proofs, a set of rules to manipulate proofs, and several motivating examples. We believe that the ability to create and manage complex scoping and dependency relationships among proofs will allow systems for formalized mathematics to more accurately reflect the natural structure of mathematical knowledge.

MKM 2005 in Bremen, Germany

Wednesday 20 July 2005 8:18 pm

One of the benefits of being a graduate student is the opportunity to travel abroad for conferences. I’ve spent the last week in Bremen, Germany at MKM 2005 presenting a paper Terese and I wrote, A Proof-Theoretic Approach to Hierarchical Math Library Organization. Not only did going to the conference afford me the chance to have another paper published, but it also gave me the unexpected and very exciting chance to see Terese again. You can see some pictures from the trip.

I had a really nice single-serving friend from Ithaca to Philadelphia in the form of Dr. Kate Whitlock, a professor at Cornell in Genetics. She was off to a conference in Germany, too, so we got to sit in the terminal in Philadelphia and chat for a bit. The flight to Germany itself seemed quite short, given that my last two international flights were to Kazakhstan and New Zealand, the latter of which included a 40-hour voyage to find my way to Wellington. An 8-hour flight? Fourteen hours in transit total? Nothing! On the flight to Germany, I had two seats to myself, meaning I could sleep comfortably. Of course, I fell asleep just in time to wake up for breakfast.

One of my worries on the trip over was customs. I hate dealing with customs and immigration and find it to be a bit stressful. However, passport control in Germany was unbelievably easy. No “what are you doing here?,” “how long will you be here?,” “can I see your return ticket?,” or “have you ever lived in Texas?” I was through customs in Frankfurt and at my gate to get on my plane to Bremen in less than half an hour. That was reassuring, as Terese was quite worried her 50-minute layover in Amsterdam would not be enough to get through customs and catch her connecting flight.

Upon arriving in Bremen, I took the tram and the train to the university. For the first time in the trip, I got to play the “I’m just a stupid American” card. Apparently, one needs to have the train ticket stamped in a little machine before getting on the train to ensure one is only using the ticket once. I was not aware of this fact and sat on the train to be on my merry way. When the woman came to check my ticket and said, “Das tickethausen nein stampened,” I simply said, “Huh? I don’t speak German.” I’m normally not a fan of coming across as incompetent and stupid, but when I get into such a situation in a foreign country, it seems like a perfectly legitimate way to get through without much trouble. Americans are all trouble anyways, aren’t we?

I made the long walk to the university from the train station and got my room ticket. MKM decided to put us up in the dorm rooms. The room was extremely bare and there was no soap nor shampoo for me to use. I was sharing a bathroom with another person, apparently spending the summer at the university, so I partook of his cleaning products…I hope he doesn’t mind. On the positive side, the room had internet in it, meaning I could keep up with the world and keep in touch with Dexter about the paper we were writing with a July 18th deadline.

After a brief nap, I went back to the airport to pick up Terese. I was happy to be able to have already done the trip so she wouldn’t have to worry about figuring out the train schedule and such. Having been more than three months since I had seen her, I was looking forward to catching that first glimpse of her as she got off the plane. From the observation deck, I saw her walk off of KLM flight 1757 and into the terminal. (I was glad to see she was in fact able to make her connection.) Smiles when our eyes found each other again for the first time in a time that was simultaneously nothing and forever.

The first order of business at the conference was the workshop. It was all about the SESAME project, some huge research grant proposal by most of the people at the workshop. As a result, Terese and I felt very out of place, as we had nothing to do with the proposal. Apparently, we shouldn’t have technically been there, but they didn’t mention the topic of the workshop until after we had registered for it. Luckily, Terese’s father and brother Daniel were coming to visit her, since this was the closest she had been to home in nearly a year. We skipped out on the afternoon sessions and went to Vegesack with them to have a drink, eat some ice cream, and walk around a bit. It was nice to see and chat with her father again, as I last saw him when Terese and I went to New York City in the fall. It turns out that he is quite the successful online poker player, so we chatted about that a bit among other things.

On Friday, I had to present our paper. We were the first to present. Being first can be nice because it means the presentation is over quickly, but it also can be slightly overwhelming, as I have never been to the conference before and I had no idea if there were “standards” I would have to meet. I never have found public speaking to be frightening, as I figure any excuse to make people listen to me for half an hour can’t be bad. Talks of this nature only make me worry that I could be exposed as a fraud, not really knowing what I’m talking about. Question sessions can be difficult because one does not know what to expect and gaps in theoretical background can put the person asking the question and the person answering on different levels making it hard to communicate. There is also the strong fear of discovering that someone else has already done the same work and I simply missed it when looking for related research. Apparently, there is some work done in the area of the paper we wrote and I need to explore it a bit further to find out if the things we are doing truly are unique.

The conference provided a variety of moments. Academics seem to be either really good or really bad at speaking. The good ones are obviously prepared, stay within the allotted time, and are dynamic and exciting. The bad ones don’t seem very interested in their own work, are obviously not well rehearsed (running over 10+ minutes), and sometimes even read straight from the paper. However, a number of the papers were interesting. Our hosts Michael and Andrea Kohlhase discussed the space of knowledge. Serge Autexier, whom I first met at LPAR in Kazakhstan two years ago, presented a great paper on a data structure for representing proof attempts. It gave me several ideas for my own work that I am eager to explore. There were also a number of memorable quotes:

  • “They believe it after talking to me for awhile.”: A presenter in Physics in response to a question about his belief on the basic unit of knowledge in his field
  • “Great people, but irrelevant.”: Describing the SESAME proposal in the eyes of the “Eurocrats” who reviewed it
  • “This is not a sexy area for undergraduate teaching.”: Referring to mathematical knowledge management.
  • “I don’t remember what the acronym stands for.”: Referring to SESAME, which stands for “Semantic Structure for Managing Mathematical Knowledge
  • “It is dangerous, but it works.”: A presenter describing some hacks he made to a system
  • “I think we’re moving into philosophy.”: Trying to stop a conversation on the value of 1/0
  • “So 0-1 = 0?”: Discussing Isabelle’s list representations
  • “Well anyway, you have to believe me.”: A presenter, when her demo crashed

After the conference was over, Terese and I spent a couple extra days in Bremen. We moved to the Inn Side Residence-Hotel at the Space Park. I’m still not exactly sure what the Space Park is, although it did have a large building with a movie theater and a rocket. The room was nice and, unlike the dorms at the conference, did not require us to move furniture. Out the window was a river and plenty of windmills. It is the first time I’ve seen windmills and they are pretty darn nifty. There is something peaceful and graceful about the way they move.

We certainly took full advantage of our time together in Bremen. The first day was spent mostly relaxing, including dinner at a Greek restaurant with some of the best meat I have had in my entire life. The moon came out to say hello to us while we were back in our room, bright and unavoidable. I said a few words to she who watches over.

On the second day, we went into downtown Bremen and walked around and shopped. I’m normally not a shopper or browser, but I very much enjoy shopping with Terese. We went to a few clothing stores such as H & M, which do not exist in Japan. Some time ago, Terese had expressed an interest in finding some clothes for me and for the first time, and after shopping there, I think it could be fun to do the same for her. She’s already had a positive influence on my fashion sense, as my pants are now actually long enough (and more comfortable as a result). The next time we see each other, we shall have to go shopping and perhaps force our tastes on each other.

On the way back to our hotel, we stopped at an Aldi to get some food, thinking we’d have a simple dinner consisting mostly of fruit. However, upon arrival at the hotel, we decided that a nice dinner in their restaurant would be better. It was a good choice, as we got to eat outside and have some excellent fish. After dinner, we went back to the room and stayed up most of the night, enjoying the little time and lots of food we had left.

The next day, our taxi picked us up at 6:50am to go to the airport. My flight left at 8:25 and Terese’s at 11:35. Our time in the airport was sad, as it always has been, trying to hold on to those last few precious moments. Despite the fact that our time together was short, despite the fact that we were leaving, despite the fact that we would not see each other again for some time, we still smiled uncontrollably. Leaving each other is certainly sad, but the sadness is accompanied by the joy of time spent together. When the time came, I went to my gate and left Terese to wait for her flight back to Japan. As the plane was pushed back from the gate, I could see her on the observation deck. I said my last good byes and shed a few tears as the Boeing 737-300 left the ground.

My trip home was relatively uneventful. I got through German departure passport control with no problems, although my laptop was subject to a special search and there was a guy with a very large gun in the terminal, which I found rather scary. From Frankfurt to Philadelphia, I was able to sleep half of the way. I was sitting next to three gentlemen who looked very much like they should be in a band together. Maybe my judgement was based on stereotypes, but they had some cool tattoos, were enjoying listening to music, and bought and consumed a large amount of Jack Daniels. I couldn’t resist and I asked the one sitting next to me if they were in a band. As it turns out, they are Playing Enemy, a group on Escape Artist Records returning from a tour in Europe. I listened to some samples on their webpage and they are a little loud and chaotic for my tastes, but they still seemed like cool guys.

Philadelphia immigration and customs proved to be the easiest I have ever gone through in the United States. It took nearly no time at all and they didn’t ask any strange questions. My flight to Ithaca was delayed two hours due to air traffic congestion. Apparently, this is quite a normal problem in the area. When we finally did get on the plane, the pilot said we’d be very lucky if we took off in an hour. It took an hour and a half of taxing and waiting our turn in line. The airport was complete chaos, with planes facing every direction to get to the single runway being used for departure. We eventually made it to Ithaca, three hours later than scheduled. My luggage, on the other hand, arrived two hours later than I did. How my luggage was not able to get from customs to the plane in over two hours is beyond me.

On the plane, I saw a rainbow below. For a time, it seemed to follow behind our plane like a pet. Shortly before we landed, I enjoyed the sunset out the left window and the moon out the right. It was as though the plane served as a conduit between which the two were speaking to each other. In that moment, I said a few more words and thank yous for the opportunity presented to me.

Overall, I’d say this trip could not have gone any better. My work was actually interesting to some people in the community. I unexpectedly got to see she whose influence and impact in my life is deep and unmistakable. I am truly lucky these days.

A Project People Actually Use

Friday 8 July 2005 6:56 pm
Top 10 Widgets When Mac OS X 10.4 came out, Apple introduced a new feature called Dashboard, which is a program to run widgets, small programs to display information or perform simple tasks. I decided I wanted to design a widget to display animated weather maps and so I took a look at the work involved (HTML, JavaScript, and CSS) and wrote the widget Radar In Motion.

Websites have popped up all over the internet for developers to upload their widgets so other users can benefit from them, including Apple’s own list. On that page, they keep track of the most downloaded widgets. Well, today the most downloaded widget is mine! It has been downloaded more than 80,000 times since I posted it in the end of June.

I’ve written a few in the past and made them available, only to have no one really use them and someone else design much better versions of the same thing. Now I’ve designed a useful program that I enjoy maintaining and that not only I use (now that I have added enough RAM to my computer to make Dashboard usable), but that other people seem to want. Maybe now I can actually call myself a computer scientist.

19 queries. 0.819 seconds.
Powered by Wordpress
theme by evil.bert