In response to my call for papers to all visiting CMU computer science professors at the University of Chile, the following paper was submitted and accepted for publication:
A Sabbatical in Santiago
The initial inspiration for our visit to Santiago was the opportunity for me to do a sabbatical working with Éric Tanter at here at the University of Chile. Well...technically CMU doesn't officially have sabbaticals, but it has faculty leaves, and with some help from my department head (thanks Bill!!), some assistance from Éric and his university (thanks Éric!!) and some funding for the collaborative research I've been working on (thanks to my generous sponsors!!) a leave can be very much like a sabbatical!
The coolest part of my time here has been the opportunity to start a fun new research project with Éric--one that we plan to continue after I return to Pittsburgh, in collaboration with Felipe Larenas, a Ph.D. student here at the University of Chile. We are working on gradual separation logic: a way of verifying that computer programs operate as intended. Inspired by gradual types--an area of Éric's expertise and a topic on which we have collaborated before--gradual separation logic combines verification that happens when a program is first written by the program, with verification that happens when the program runs, in a seamless way. Separation logic--which was co-developed by my colleague John Reynolds at Carnegie Mellon, by the way--is the state of the art in verifying written programs, but combining verification of the written program in separation logic with run-time verification is a wide open area. So we're very excited about the possibilities of the project!
A second part of my sabbatical goals has been having a chance to get in touch with my inner coder. While there's always too much to do--even on sabbatical--I've had a chance to do a fair bit of this. In the category of "ordinary hacking" I've been working on a new front-end architecture for Wyvern, the programming language my group is working on. Whitespace is significant in Wyvern's syntax in a way that depends a bit on parsing, so there is a tighter tie between two phases of the compiler--called lexical analysis and parsing--than in many programming languages. After some discussions with the team in Pittsburgh--notably including Benjamin Chung--we came up with a good architecture that will enable us to separate these phases cleanly and still handle whitespace properly. I've made good progress on prototyping the new lexical analyzer, which will enable all this to work.
Even more interestingly, I've been working my way through Pierce's Software Foundations course, learning to write proofs and programs in Coq. The Coq language is becoming a standard tool in programming language and verification research, so it's a good tool to know, and it has been fun learning it. This also opened a good opportunity to talk with Éric and Nicolas Tabareau, who was visiting from INRIA, about encoding objects in Coq. In the process, we are in the process of discovering some interesting new characteristics of objects that came out of the translation...more details will perhaps come in a paper when we can refine the ideas!
A sabbatical is also a chance to renew and recharge. BB has written about many of the fun things we've done as a family, and we have found many truly amazing places in Chile to which we hope to return. The kids have been doing a different kind of learning, both from their cultural experiences here and in the home school we have been doing together. Particularly fun for me has been teaching the kids to write computer programs, using the amazing tools at code.org. They understand the basic concepts of computing already, and have each written some fun games. This is one of the things I hope we can build on together when we are back in Pittsburgh.
For me, personally, the sabbatical has also been a chance to learn about myself and reflect. One significant area of reflection has been on the nature of time and how to manage it. When I began my sabbatical, I shed a number of commitments and anticipated that I would have freedom to spend my time in different ways. The reality was not quite what I hoped. I did, of course, have the time to undertake some of the explorations above, and I was able to be much less stressed about my life in general, which was renewing and which also facilitated my reflection. On the other hand, I learned that time commitments are long-term, complex, and not always explicit--involving choices I have made in how I structure and fund my research and how I serve the communities I am a part of. As a result, although many of the things I did were interesting and worthwhile, I did not have as much flexibility with my time as I had planned. While this was somewhat disappointing, it also presents an opportunity for me to think in a more strategic and long-term way about my time investments in the future. This opportunity is also a good thing for me to take away from my sabbatical.
No comments:
Post a Comment