gregory m. malecha
gmalecha {at} eecs.harvard.edu School of Engineering and Applied Sciences, Harvard Universitynews
I'm a Ph.D. student in Computer Science doing research in programming languages at Harvard University. The goal of my research is to better understand programming languages in order to make it easier to write correct programs which can be compiled to run efficiently.
After much too long working on proofs for a B+tree, i've finally figured out what is making my tactics so slow; it's omega. This file takes about 42 seconds on my desktop and consumes almost a gigabyte of RAM.
My temporary fix/workaround is to rewrite a bunch of stuff before passing the equation off to omega; it seems to do well for the example, but i have no idea how it will perform on everything else. here's to hoping (crossing fingers).
With the research group at Harvard I've been working on imperative programming in Coq based on Hoare Type Theory (see the Ynot project, out of date). We've built simple echo and prefix evaluation servers which will form the basis of a web-server which we're hoping to finish by the end of January (current code).
I finished my fellowship application on Wednesday morning and got it turned in. I think it turned out pretty well. Also need to do the NDSEG fellowship but that one isn't due until January so I've got a few months.
Other than that, there was a very interesting talk about Distributed Live Objects given by Daniel Margo for the systems group on Friday. It was good, and I'm looking forward to the colloquium this Thursday by Ken Birman.
I've spent basically the entire last week writing NFS essays. I've gotten lots of feedback on my essays but there's still a lot more to do. The deadline is Nov. 5th so it looks likes I've got a little while longer to write.
The news system seems to work now. It's based on files in a directory which are named with a timestamp, not too bad of a system---at least it makes it easy to make them manually.
I've been meaning to get a news system built for a little while, and I figure a short break from important life will do me good. I'm a little annoyed that the Harvard servers don't support XSL which would make all of this completely easy, but maybe if I can migrate things at some point it will work out better.