Tuesday, Feb. 1, 12:30 (approx) pm: Peter Sewell of the University of Cambridge will be giving an informal talk on the 20th floor of the UT Tower on Tuesday, Feb. 1. The talk will be about concurrent memory models and program verification - he and his collaborators have been working on hardware models (for x86, Power, and ARM), on language models (especially the proposed C++0x/C1X model), and on compiler verification. He plans to arrive at about 12:30 pm and the talk will begin shortly thereafter, ending around 2pm more or less. He and his colleague Susmit Sarkar will be available for further discussion till about 2:30 pm. They're especially interested in talking about extending their models to cover more x86 features (interrupts, page tables,...). Feel free to bring a lunch.