Project

In summer '08, I served as a Research Assistant at the University of Pennsylvania for 10 weeks through the CRA-W DREU program. DREU is the Distributed Research Experience for Undergraduates sponsored by CRA -W. My mentor and I were also mentioned in the CRA Summer-Fall 2008 newsletter.

Click here to download a PDF version of my final report.

My Mentor
In Summer '08 I worked with Dr. Stephanie Weirich at the University of Pennsylvania. Her research interests include statically-typed programming languages. Her current research projects include type-directed programming, type inference for advanced systems, and machine assistance for programming languages.

My Research
With Stephanie, I focused on exploring the properties of dependently-typed programming languages. I explored the implementation of different algorithms of binary search trees in these languages and its implications.

Journal

May 26 - June 1
I am in Philadelphia. A year ago, if someone would have told me that I would be interning in Philadelphia, I would have thought that me winning a Turing Award was more likely. Maybe I will win a Turing Award. But for now, I am in Philadelphia. I am writing this less than 12 hours away from meeting my mentor Dr. Stephanie Weirich (provided I can find Levine Hall tomorrow). I should be sleeping, but I am still on Fort Worth time. 11:48 pm is too early to go to bed for a college student. Especially a Computer Science major. But I want to blame part of the restlessness on nerves. Why should I be nervous? Its only my first internship. Its only in a city I have not spent more than 2 days in. Its only a few thousand miles from home. Do I need to go on?

Saying goodbye to Fort Worth was hard, even though I will only be gone for 10 weeks. I made a point to walk through the science and technology building, Tucker Technology. I have spent many days and nights there. My friends have a running joke that I have "all-night access to Tucker." So true.

So, good bye Fort Worth for 10 weeks. Hello Philadelphia and UPenn for 10 weeks. What will happen next? Something tells me it will be life-changing. But I would check back in a week if I were you. :)

June 2 - June 8
I am still in Philadelphia. After three meetings with my mentor, Stephanie, I am extremely excited about the next few weeks. The first two meetings were spent brain-storming about possible summer projects. I finally decided that analyzing properties of dependently typed languages seemed like an interesting subject. I have no background whatsoever in functional programming languages, so this decision is mainly influenced by the experiences I have had with Coq (a functional language that is used as a proof-assistant) and the first three chapters in "Types and Programming Languages" by Benjamin Pierce. But Stephanie said that I had every right to complain about it if I thought I was not meant for dependently typed programming languages. So, here's to hoping for a successful relationship with the above-mentioned languages.

My background will come into play a lot with this project. I will get a chance to test algorithms I am aware of to study the behavior of dependently typed languages. So, in a sense, I have a lot of freedom in the way I choose to analyze these programming languages.

That was everything I have discovered about my project. I also discovered that lambda calculus cannot be learned easily. My question to Stephanie, "How the hell am I supposed to do this?" (I can be very blunt sometimes). Her response, "It just happens." Hopefully, it will happen next week.

I also went to the weekly PL Club Meeting. That is where graduate students and professors meet to discuss a paper as chosen by the presenter (a member of the PL Club). We discussed Gordon Plotkin's "Call-by-Name, Call-by-Value, and the Lambda Calculus" which is thought to be a ground-breaking paper in this "world". It was the first time I had heard of it (seeing the heavy background I have in type systems ;) ), however I felt reasonably at home with all the PL jargon being thrown around. Having more than a week's worth of knowledge would have been nice, but we are discussing the second part of the same paper next week, so it should be fun (in the most normal CS sense of the word "fun").

I also discovered the trucks outside the buildings on campus. They have the most amazing yet cheap food you could imagine. I wish they had those back in Fort Worth!

Another ground-breaking discovery was the whole living-in-the-city experience. I have two Starbucks (very very important), a Gap, Ann Taylor Loft (very important), CVS, Boston Market, Grocery Store, and numerous other eateries within walking distance. My life is complete! :) I also rode the Subway for the first time on this Continent (I have ridden the subway in Singapore before). And I explored downtown. This city has so much history! I saw Independence Hall, the Second Bank of the United States, a random 18th century-style garden, and many other sights. I need to go back downtown very soon. There are so many amazing places I haven't seen yet!

So, yes, I love Philadelphia. It is a drastic change from Fort Worth with the big CS department and the city environment, but it a very good change for me. I plan to go to NY next weekend, and make some headway into my research. More experiences coming soon!

June 9 - June 15
So, Monday morning was spent reading extremely carefully about the enigma called Lambda Calculus. Prior to this week I was completely at loss as to how to approach it. But a few hours and various permutations and combinations later, it finally made sense. The answers at the back of the textbook were slightly helpful as well. ;)

I spent the first half of the week reinforcing all the information I have learned over the past 10 days. Not very stimulating since the initially excitement of learning them wasn't there, but I knew it had to be done.

I met with Stephanie on Thursday. We spent an hour and a half talking about, well, everything. She will be out of town next week, so she was anxious about making sure I knew what I was doing and that I had something to do. We decided that I will actually to implement algorithms (searching, sorting, etc) in Coq. Figuring what properties I could prove out them was the next step that was to be performed simultaneously. After that, I would actually attempt to prove them. So, I have a game plan! Oh, and, at the same time, I continue to read the textbook, and another algorithms book, the Coq tutorial, Coq lecture notes from a graduate class at UPenn, and a preview of a textbook (on Coq) by Benjamin Pierce, a professor at UPenn. So, I think I should have various "fun" (refer to my previous entry for my definition of fun) tasks to perform.

There was also another PL club meeting this week. I had mentioned earlier that we continued to discuss last week's paper. My previous comments still hold. :)

So, that was research. What about fun? Well, nothing much. I just spent the weekend in New York with one of my best friends. And it wasn't' "fun", it was supercalifragilisticexpialidocious! We walked and walked and walked everywhere! Times Square, Fifth Avenue, Brooklyn Bridge, Bronx Zoo, Queens Botanic Garden, United Nations, Grand Central, Chinatown, Little Italy, Madam Tussauds, M&M store, Hershey's store, Flushing Meadows, NY Hall of Science, and a Broadway show (Mary Poppins)! I think that is the complete list. :) I think you get the idea. It was one of the most amazing weekends ever! So, next week = more research (aka reading, hacking, thinking), a lunch with the 20 other CS undergraduate Research Assistants working at UPenn (Geek Time!), and a weekend off (hopefully). Till then, docious-ali-expi-listic-fragi-cali-repus!

June 16 - June 22
Three weeks have gone by so quickly! I wish the weeks would slow down; I really do not want the summer to end.

What did I do this week? Well, I read Benjamin's draft of a textbook he is writing (which is completely related to my research). I also gave him feedback on it and found it intriguing to hear about another person's experiences with functional programming. I also worked on his online lectures from the graduate course I have been learning Coq from. I spent three hours today attempting to prove that "plus m m = plus n n -> m = n" aka "if m+m = n+n, m = n." Doesn't sound too hard, does it? Well, it was one of those things where I couldn't see what to do. And I had the solution set minimized in the background, but for some reason I was determined to work on it till I figured it out. Three hours later I realized I probably wasn't going to figure it out today, but it was fun struggling with a problem. I finished the next five proofs in an hour. Contrast much? So, I am done with Lecture 6. Moving on to Lecture 7.

I also plan to work on implementing linked lists, arrays, sorts, and other data structures in Coq / ML. One more hacking session will be underway soon. I was up all night this Wednesday (working on Coq), and I saw the sun rise! I haven't seen a sun rise in so long! And it was so pretty from the twenty-second floor!

Next week I will hopefully have something more entertaining to report. More research will be done (hopefully by me), and I will probably gush about spending next weekend in Boston with an old friend.

Till then, ciao!

June 23 - June 29
It feels like I was writing about the beautiful sunrise yesterday. But, alas, it was a week ago. It was a mixed week for me.

I started off attempting to understand how to implement data structures in Coq. That didn't really happen, even with a relevant book Stephanie gave me. So, then I decided to use my favorite research tool: Google. WIthin a few minutes I had 20 tabs open, and I was staring blankly at an implementation of binary trees. This lack of comprehension lasted for a 2 days. Finally, during one of my meetings with Stephanie, she walked me through 2 or 3 functions, and showed me how that code actually did what the comments said it did. So, I am set to conquer slightly more complicated data structures. I also finally figured out how to work through Benjamin's lectures at a decent pace. Most of the proofs in the first 8 chapters clicked. Only problem is that my perennial habit of forgetting is still around. So, I am in the process of redoing it. Benjamin's notes are diverging away from my research, but I still really want to read them, so I will work through them anyway.

As for fun, I spent the weekend in Boston visiting old friends from High School. I also walked on the Freedom Trail, enjoyed the Sunset Cruise, marveled the realistic glass flowers at the Harvard Museum of Natural Science, explored my geeky side at the MIT museum, played with CS legos at the Museum of Science, walked down Newburry Street, roamed the esteemed halls of MIT and Harvard, and enjoyed Monet's work at the Museum of Fine Arts. Not a bad way to spend the weekend. Again, I will have to whittle down the pictures to 1/80 their initial value, so they will be up as soon as I get a chance.

This week I plan to experiment some more with Coq. My research is finally starting to look like "research:" (quoting a friend) hacking on code that may (not) be commented and may (not) work to see if I can (not) make it do what I need it to do. I will (not) give up.

June 30 - July 6
Halfway there! It has been an absolutely crazy set of five weeks, and I can't wait to see what the next five weeks have in store for me.

Research-wise this was one of the weeks you didn't want to be a research assistant. My current task is to read up on some Coq code and attempt to code something original. I am also reading Benjamin's notes and textbook for fun on the side. I am at the point where I understand the Coq, but my head is refusing to take the next step. So, hurrah research!

My weekend was quiet. I spent time with family (my sister visited), and I watched the fireworks from my living room window (being on the 22nd floor has its advantages). My sister and I were more interested in not getting wet in the pouring rain rather than seeing John Legend preform.

I have to write my half-way report this week. And so does Stephanie. So, hopefully I will have something interesting to say! Later. : )

July 7 - July 13
I just finished writing by half-way report. I was looking forward to documenting everything I hadn't done, but then I realized that list wasn't too long. I also realized that I am having a great summer. : )

Research was great this week. I was as stressed out as I get during finals week, but it was still fun. I think I finally crossed the hurdle I had been facing for the past few days. My current task is to analyze rmax, a function to delete the largest node in a binary search tree, and write and prove it in as many ways I can think of. So, I will to get in touch with my inner creativity over the next week. And this is when the real hacking starts, where I can spend hours over 5 lines of code. My favorite part of research.

I also got to attend two research talks this week which was fun. The first was about representing programming languages, and how polarity was the difference between call by value and call by name languages. I found it enthralling as I am a closet math fan. Stephanie also provided me with a paper on it, so I have bed time reading for the next few days. The other one was given by a graduate student at UPenn, and it was about how a simple language can be used to represent complex ideas by building up on it. The paper had really simple ideas, but these ideas had a huge impact 40 years ago.

I went to the UPenn Museum of Archaeology and Anthropology today. I spent two hours dreamily walking around artifacts from thousands of years ago. They have a good collection of items from around the world.

Next week will be challenging, but I am looking forward to being challenged!

July 14 - July 20
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 21 - July 27
Only two more weeks! This week was nearly a repeat of last week. I worked on rmax, Program, and a few more Coq proof tactics. I haven't made any startling discoveries yet (good or bad), but lets see if this week is my lucky week! The to-do list for next week is the same: rmax, Benjamin's class notes, and Program. I also attended another PL Club meeting. This week was about Robin Milner's views on the implementation of polymorphism. This summer, the theme of the club is important works in programming languages, so, like the other papers we have talked about, it was a big step in programming languages in the 80s. I visited my best friends from TCU in NY this weekend. After that break, I am looking forward to working on my different research puzzles.

July 28 - August 3
Need I say, only one more week!!! Ahhh!!! Coq treated me relatively well last week. I worked on rmax and also researched some more ways rmax and remove functions have been implemented in Coq. I worked through a few chapters in Benjamin's notes and got to the fun part, inductive principles aka 3- 4 line statements I have to read 5 + times to understand. But I did the chapter twice, and I have my fingers crossed that the information I read will be retained. : )

I also played around with Program. It wasn't quite as fun as working Benjamin's notes or hacking on whimsical proofs, but it was an interesting experience. Next week I hope to get everything I have worked on together so that I can write a decent final report. I will probably write the report after the 10 weeks though. Lets see what Stephanie has to say!

I explored a little bit of Philadelphia this weekend. I hit a few of the tourist spots (Independence Hall, etc). And I have also been working on a to-do list for Fort Worth (when I get back) which is growing exponentially. My inbox has a few more emails than I would like.

So, next week is the last official week I will be working on Coq. I hope it isn't because I think I will keep hacking on proofs once school starts. There is a barbeque and a lecture I really want to attend next week. The lecture is a public lecture from ICHEP on high energy particle physics. I audited quantum physics for fun a few semesters ago, so I do have an healthy/ unhealthy interest in quantum physics as well. Till next week, toodles!

August 4 - August 10
Last week was like finals week.. only worse. Before the week started I knew I had to start writing my final paper, finish my research, say goodbye, and pack. On Tuesday, I also found out that I had the opportunity to present my research to the graduate students and professors in the programming languages department at UPenn. Of course, I jumped at the chance, but that added a few more items to my already long to-do list: figure out what I was going to speak about. make slides, practice my presentation, overcome the numerous thoughts of doom going through my head, and actually give the presentation. I am good at public speaking, but in this instance I was more afraid of the audience in the presentation than the fact that I was giving a presentation.

I wrapped up my research on Tuesday. We finally had another version of rmax that worked. The cool thing was that it completely reflected the inner workings of the algorithm. Tuesday was also when I found out about my presentation, so in between by 11 o'clock meeting with Stephanie on Tuesday to my 3 o'clock meeting with her on Wednesday, I put the finishing touches on the proof. I spent a few hours cleaning it up and analyzing the proof. I also worked on comparing the two proofs: the proof from the Coq official website and the modified proof. I set up my slides, and I churned out a rough draft of my paper.

Five more rehearsal presentations and 72 hours later, it was Friday, my throat was extremely sore, and I had a presentation to give. I think it went well. Stephanie didn't have any major complaints. And everyone else in the room seemed intrigued, and laughed at some of my jokes.

After the meeting, I wrapped up the loose ends with Stephanie. I will have my final paper ready in little less than a week, and that will be a more formal version of the research I have been describing over the past few weeks.

I went downtown on Friday to celebrate and reward myself for the intense 10 weeks. I also sat for a very long time in front of the fountain in Love Park (my favorite fountain ever!). I spent the weekend with my Aunt and Uncle in New Jersey. My cousins took good care of me for the weekend, and right now I am at the airport, waiting for my flight. My plane is currently delayed indefinitely because of bad weather ( the airport is closed). I have my fingers crossed!

Philadelphia treated me really really really well! UPenn was amazing, the campus was gorgeous, Stephanie is one of the most awesome professors I know, and the PL department at UPenn is the most stimulating environment I have ever been in. My travels added to the fun part of the summer; New York, Boston, and DC were amazing experiences! This summer changed my life and shaped my dreams, and I can't wait for graduate school!

Pictures