Termination research now VERY fashionable ;-)
I'm mentioned in Vogue in an article about Tauba. Dec '08....the year termination research become fashionable ;-)
no kidding, functional programming has really arrived.....
Watching this talk gave me shivers. My love (functional programming) is now mainstream. Very funny talk, by the way.
Eric Koskinen
Welcome to Eric Koskinen, who just started his PhD at Cambridge University under the supervision of myself and Matthew Parkinson.
Professor Cook
Queen Mary, University of London has now appointed me as full professor of computer science. I'm not leaving Microsoft, of course, its a joint appointment with Microsoft Research.
methods of proving recursive programs terminating
I'll state this perhaps a bit too strongly (to make the point). Recursion, and program termination, are completely orthoginal issues. Check out our new paper: CFL-Termination. This paper shows you how (if you have an oracle for partial correctness semantics) you can convert recursive programs into semantically equiv. non-recursive programs without tricky encodings using heap or non-linear updates to arithmetic variables. Enjoy ;-)
F# release
Check out the community technology preview (i.e. pre-release of the "productized" version) of F#.
vacation.....actionscript
I'm on vacation/holiday......during my time off I've learned actionscript/flash programming. Aubrey and I wrote a game. See the result.
Paper on non-blocking algorithms
See our new paper: Proving that non-blocking algorithms don't block.
Balance.....
"It has long been my personal view that the separation of practical and theoretical work is artificial and injurious. Much of the practical work done in computing, both in software and in hardware design, is unsound and clumsy because the people who do it have not any clear understanding of the fundamental design principles of their work. Most of the abstract mathematical and theoretical work is sterile because it has no point of contact with real computing. One of the central aims of the Programming Research Group as a teaching and research group has been to set up an atmosphere in which this separation cannot happen. "
- Christopher Strachey
- Christopher Strachey
Finishing.......starting...........change..........
Congrats to my family: Aubrey graduated from primary school, Mina graduated from childhood; Bee is soon to be the shortest member of the family. ;-) Now we begin new adventures......
FMSB, WG2.3, Andrey, etc...
Why travel to conferences when all of the interesting people and meetings come to me? This summer's examples include Formal Methods in Systems Biology, WG2.3, Workshop on the Verification of Concurrent Algorithms, and visits by Andrey, Mooly and others.......
Rebooting "Communications of the ACM"
I was impressed by Moshe's article on upcoming changes to the CACM.
Imperial lectures, details.......
I will be giving 6 hours of lectures on `Proving termination and liveness of programs' at Imperial, in London. The times are 2-4 on Tuesday 27th May, Wednesday 28th May and Thursday 29th May in Room 145.
Good luck to Jim Larus!
Jim Larus dropped by our lab this week and gave us the rundown on Dan Reed's "Data Center Futures" group that he has joined.......
Automated reasoning group
On tuesday I'm giving another talk at the Automated Reasoning
Group's lunch talk series....
Group's lunch talk series....
A long time coming.....
Sometimes I find solutions to research questions to be very easy to find (e.g., we concieved and wrote up the paper "Proving thread termination" in perhaps 24 hours). This however was not the case for my new CAV paper "Proving conditional termination". You may find it simple now, but for some reason it took us years to develop this idea.
The research on this topic began as a conversation in 2006 between Mooly and I (in Tom Ball's office) after the first talk I gave at MSR-Redmond on Terminator. As visitors
to my lab came and went (e.g. Mooly, Sumit, Andrey, Tal) the thing snowballed into an ever growing ruckus carried out over visits and conference calls......co-authors would disagree and go off and write their own drafts, argue, plead, make alliances against each other, etc. It was terrifically fun, but I began to wonder if we'd ever find a workable solution. Finally, this winter, we got some traction and developed essentially what is in the paper today. After many many drafts, many failed starts, etc, the final version of the paper is finally done. Sigh.
Mooly is coming back to my lab this week.......I wonder what troublesome research question he'll propose this time ;-)
The research on this topic began as a conversation in 2006 between Mooly and I (in Tom Ball's office) after the first talk I gave at MSR-Redmond on Terminator. As visitors
to my lab came and went (e.g. Mooly, Sumit, Andrey, Tal) the thing snowballed into an ever growing ruckus carried out over visits and conference calls......co-authors would disagree and go off and write their own drafts, argue, plead, make alliances against each other, etc. It was terrifically fun, but I began to wonder if we'd ever find a workable solution. Finally, this winter, we got some traction and developed essentially what is in the paper today. After many many drafts, many failed starts, etc, the final version of the paper is finally done. Sigh.
Mooly is coming back to my lab this week.......I wonder what troublesome research question he'll propose this time ;-)
Proving conditional termination
Here are the slides from a talk on proving conditional termination that I gave at CMU.
CAV papers......
I co-authored a couple of papers that will appear at this year's CAV conference:
- Proving Conditional Termination, with Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sagiv
- Scalable Shape Analysis for Systems Code, with the East London Massive
Terminator at Techfest keynote speech
Rick Rashid (Senior VP of Microsoft Research) discusses Terminator, termination, and liveness in his TechFest keynote address. See the video (at 29m into the talk).
Imperial lectures
I'll be giving a mini-course on proving program termination/liveness at Imperial, May 26th, 27th, and 28th, from 2-4pm. If you're in the London area you're welcome to come, to send students, etc. These lectures will be a condensed version of the 14 lectures on the same topic that I gave at Carnegie Mellon this winter, and preliminary version of what I will give at Marktoberdorf this summer.
Final week at CMU, returning to Cambridge
This is my final week at CMU. On wednesday I go to Baltimore to attend the NSA's HCSS meeting (where I will give a talk and sit on a panel), and then I return to Cambridge.
My visit to CMU was fantastic. Thanks to Ed Clarke, Jeannette Wing and Randy Bryant for the invitation, and to Peter Lee, Randy Bryant, and Denny Marous for making it happen. I worked with a number of great people, learned a lot, and made many new connections. It was an exciting time to be at CMU, especially given the recent announcement about this year's Turing prize winners.
My course seemed to go remarkably well, especially considering the lack of introductory papers/books from which to draw material. I can confidently assert that my course was the most in-depth course on termination/liveness ever taught before......with 14 lectures covering topics such as well-founded relations, decomposition techniques, rank function synthesis, invariance and variance analysis, refinement, inductive proof techniques for termination, termination for recursive and concurrent programs, and fair termination. Throughout the course I had numerous bright people in the audience asking questions and participating in discussion. Special thanks to the core group (those that attended nearly all of the lectures): Stephen Brooks, Sager Chaki, James Ezick, Arie Gurfinkel, Will Kleiber, Neel Krishnaswami, Stephen Magill, Sean McLaughlin, Frank Pfenning, John Reynolds, Robert Simmons, Jiri Simsa, Michael Tschantz, and Kwangkeun Yi.
Note: Upon hearing about my course at CMU, several people outside of CMU have asked for copies of notes and/or slides. I am currently preparing a more polished version of the notes, please contact me if you would like to see a draft when I'm happy with it........
My visit to CMU was fantastic. Thanks to Ed Clarke, Jeannette Wing and Randy Bryant for the invitation, and to Peter Lee, Randy Bryant, and Denny Marous for making it happen. I worked with a number of great people, learned a lot, and made many new connections. It was an exciting time to be at CMU, especially given the recent announcement about this year's Turing prize winners.
My course seemed to go remarkably well, especially considering the lack of introductory papers/books from which to draw material. I can confidently assert that my course was the most in-depth course on termination/liveness ever taught before......with 14 lectures covering topics such as well-founded relations, decomposition techniques, rank function synthesis, invariance and variance analysis, refinement, inductive proof techniques for termination, termination for recursive and concurrent programs, and fair termination. Throughout the course I had numerous bright people in the audience asking questions and participating in discussion. Special thanks to the core group (those that attended nearly all of the lectures): Stephen Brooks, Sager Chaki, James Ezick, Arie Gurfinkel, Will Kleiber, Neel Krishnaswami, Stephen Magill, Sean McLaughlin, Frank Pfenning, John Reynolds, Robert Simmons, Jiri Simsa, Michael Tschantz, and Kwangkeun Yi.
Note: Upon hearing about my course at CMU, several people outside of CMU have asked for copies of notes and/or slides. I am currently preparing a more polished version of the notes, please contact me if you would like to see a draft when I'm happy with it........
F# team is hiring
--------------------------------------------------------------------------------
From: Don Syme
Sent: Wednesday, January 30, 2008 7:29 PM
To: FSharp Discussion
Cc: Programming Languages Interest Group
Subject: The F# team is hiring!
Hi all,
The F# team continue to have a number of positions open for compiler and language tools experts. Positions are by default in Redmond.
If you're interested in helping to bring a typed functional programming language into Visual Studio and think you have skills and commitment relevant to the achieving this, then please contact me or another member of the F# team to see if there might be a fit. If there's no immediate fit, then there may be one later, so don't be shy. We're looking for compiler experts, including optimization, type checking, performance and correctness language tools experts, e.g. experienced with language services and Visual Studio language tools QA/test experts
Kind regards
Don
From: Don Syme
Sent: Wednesday, January 30, 2008 7:29 PM
To: FSharp Discussion
Cc: Programming Languages Interest Group
Subject: The F# team is hiring!
Hi all,
The F# team continue to have a number of positions open for compiler and language tools experts. Positions are by default in Redmond.
If you're interested in helping to bring a typed functional programming language into Visual Studio and think you have skills and commitment relevant to the achieving this, then please contact me or another member of the F# team to see if there might be a fit. If there's no immediate fit, then there may be one later, so don't be shy. We're looking for compiler experts, including optimization, type checking, performance and correctness language tools experts, e.g. experienced with language services and Visual Studio language tools QA/test experts
Kind regards
Don
Pittsburgh: the friendliest town ever?
I travel a great deal. Some cities will remain legendary in my mind for their hospitality during my frequent visits. Cities deserving extra special mention include NYC, Baltimore, Paris, Seattle, SF. Other cities are HORRIBLE to visit. San Diego comes to mind (sorry, nice weather, but "pass!"). Edinburgh is pretty but (based on 3 or 4 trips that I've made thus far) emotionally cold.
I've been happily surprised at the level of hospitality that I've encountered here in Pittsburgh. Many CMU people have invited me out to dinner, or to their homes. Old friends who now live in Pittsburgh have taken me out to shows, bars, etc. Tonight I had many social invitations: a concert, a dinner, etc. I'd already made plans to hang out with Lli (old Portland friend since 1996?). Tonight was the "gallery crawl" in downtown Pittsburgh, Lli and I ended up spending our entire gallery crawl time at this gallery. We also drove around a bit and talked, and went to dinner.
I've been happily surprised at the level of hospitality that I've encountered here in Pittsburgh. Many CMU people have invited me out to dinner, or to their homes. Old friends who now live in Pittsburgh have taken me out to shows, bars, etc. Tonight I had many social invitations: a concert, a dinner, etc. I'd already made plans to hang out with Lli (old Portland friend since 1996?). Tonight was the "gallery crawl" in downtown Pittsburgh, Lli and I ended up spending our entire gallery crawl time at this gallery. We also drove around a bit and talked, and went to dinner.
All settled in at CMU
For the past week I’ve been settling in at CMU. I’m teaching a graduate course on termination (and writing some companion lecture notes). I've been meeting with the many smart professors/students/researchers. I'm also working on several papers.
For the first few days I stayed in John Reynolds’ amazing house. Then I found my own place. The neighbourhoods here are great, and the houses are HUGE by my UK/Seattle standards.
I have a great office which rivals the office I have at MSR-Cambridge, with a great view!
For the first few days I stayed in John Reynolds’ amazing house. Then I found my own place. The neighbourhoods here are great, and the houses are HUGE by my UK/Seattle standards.
I have a great office which rivals the office I have at MSR-Cambridge, with a great view!
PhD students: its time to apply for the Marktoberdorf summer school
Note: its now time to apply to attend Marktoberdorf.
Subscribe to:
Posts (Atom)