Reading Group POPL 2010
From PLSwiki
We read, present, and discuss selected papers to be presented at the POPL 2010 conference.
Contents |
Format
The idea is to reserve 1 hour per paper. The assigned speaker will give a presentation of the paper - it doesn't have to be with slides; it is fine just to do it informally on the board. Other participants are expected to have at least skimmed the paper being presented, and, if they know something about the stuff in the paper, help the rest of us understand, by giving comments during the time allocated for the paper.
News and Changes
Important and just-in-time changes will be mailed (to pls_grp, Peter, Andrzej and Jonas) in addition to being posted here.
- 4/12: "Verifying event-driven programs..." are out and step-indexed models are in on December 8th. Cf. schedule and mail from Lars dated December 4th.
- 1/12: Paper swap: "Nominal System T" and "Verifying event-driven programs..." have changed places.
- 27/11: Links to all internet available papers added by Kasper. I'll try to obtain the remaining three papers from the authors.
- 27/11: Links and rooms for first two papers added. More will follow.
- 27/11: Homepage up and running!
Comments and Corrections
Corrections and comments to this page and administrative stuff in general should be mailed to Jacob.
Schedule
Note: Schedule is tentative and may be subject to changes.
| Date | Time | Room | Paper | Presenter |
|---|---|---|---|---|
| Nov. 30 | 15:00-16:00 | Aud. 4 | A Relational Modal Logic for Higher-Order Stateful ADTs. By Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal. | Derek D |
| Dec. 1 | 10:00-11:00 | 4A05 | A Theory of Indirection via Approximation. By Aquinas Hobor, Robert Dockins, Andrew Appel. | Jacob T |
| Dec. 8 | 10:00-11:00 | 4A09 | On the essence of step-indexed models. Cf. mail from Lars Dec. 4th. | Lars |
| Dec. 8 | 11:00-12:00 | 4A09 | Structuring the verification of heap-manipulating programs. By Aleks Nanevski, Viktor Vefeiadis, Josh Berdine. | Kasper |
| Dec. 15 | 10:00:11:00 | 4A09 | Toward a Verified Relational Database Management System. By Ryan Wisnesky, Gregory Malecha, Avraham Shinnar, Greg Morrisett. | Alexandre |
| Dec. 15 | 11:00-12:00 | 4A09 | A Verified Compiler for an Impure Functional Language. By Adam Chlipala. | Anders |
| Dec. 22 | 10:00-11:00 | 4A09 | Automatic Numeric Abstractions for Heap-Manipulating Programs. By Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay. | Jonas B |
| Dec. 22 | 11:00-12:00 | 4A09 | Modular Session Types for Distributed Object-Oriented Programming. By Simon Gay, Vasco Vasconcelos, Antonio Ravara, Nils Gesbert, Alexandre Caldeira. | Søren D |
| Jan. 5 | 10:00-11:00 | 4A09 | Monads in Action. By Andrzej Filinski. Available from within ITU in ~thamsborg/teaching/popl10-mia.pdf. Otherwise mail me. | Andrzej F |
| Jan. 5 | 11:00-12:00 | 4A09 | Modular Verification of Security Protocol Code by Typing. By Karthikeyan Bhargavan, Cedric Fournet, Andrew Gordon. Available from within ITU in ~thamsborg/teaching. Otherwise mail me, it is not really for me to put in online as the authors haven't so far. | Thomas |
| Jan. 12 | 10:00-11:00 | 4A09 | Decision Procedures for Algebraic Data Types with Abstractions. By Philippe Suter, Mirco Dotta, Viktor Kuncak. | Peter Sestoft |
| Jan. 12 | 11:00-12:00 | 4A09 | Nominal System T. By Andrew Pitts. | Rasmus M |
