Thursday January 10
Invited talk, 9.00-10.00
Session 1, 10.30-11.30
ENGINEERING FORMAL METATHEORY
Brian Aydemir, Arthur Chargueraud, Benjamin C. Pierce, Randy Pollack
and Stephanie Weirich
FORMAL VERIFICATION OF TRANSLATION VALIDATORS. A CASE STUDY ON
INSTRUCTION SCHEDULING OPTIMIZATIONS
Jean-Baptiste Tristan and Xavier Leroy
MUCH ADO ABOUT TWO (PEARL)
Janis Voigtlaender
Session 2, 12.00-13.00
CONTEXTUAL EFFECTS FOR VERSION-CONSISTENT DYNAMIC SOFTWARE UPDATING AND
SAFE CONCURRENT PROGRAMMING
Iulian Neamtiu, Michael Hicks, Jeffrey Foster and Polyvios Pratikakis
HIGH-LEVEL SMALL-STEP OPERATIONAL SEMANTICS FOR TRANSACTIONS
Katherine Moore and Dan Grossman
SEMANTICS OF TRANSACTIONAL MEMORY AND AUTOMATIC MUTUAL EXCLUSION
Martin Abadi, Andrew Birrell, Tim Harris and Michael Isard
Session 3, 14.30-15.30
SEPARATION LOGIC, ABSTRACTION AND INHERITANCE
Matthew Parkinson and Gavin Bierman
ENHANCING MODULAR OO VERIFICATION WITH SEPARATION LOGIC
Wei-Ngan Chin, Cristina David, Huu Hai Nguyen and Shengchao Qin
CYCLIC PROOFS OF PROGRAM TERMINATION IN SEPARATION LOGIC
James Brotherston, Richard Bornat and Cristiano Calcagno
Session 4, 16.00-17.00
THE INTENSIONAL CONTENT OF RICE'S THEOREM (PEARL)
Andrea Asperti
A LOGICAL ACCOUNT OF PSPACE
Marco Gaboardi, Jean-Yves Marion and Simona Ronchi Della Rocca
LIGHTWEIGHT SEMIFORMAL TIME COMPLEXITY ANALYSIS FOR PURELY FUNCTIONAL
DATA STRUCTURES
Nils Anders Danielsson
Friday January 11
Invited talk, 9.00-10.00
Session 5, 10.30-11.30
PROVING NON-TERMINATION
Ashutosh Gupta, Thomas Henzinger, Rupak Majumdar, Andrey Rybalchenko
and Ru-Gang Xu
SUBCUBIC ALGORITHMS FOR RECURSIVE STATE MACHINES
Swarat Chaudhuri
BACK TO THE FUTURE: REVISITING PRECISE PROGRAM VERIFICATION USING SMT
SOLVERS
Shuvendu Lahiri and Shaz Qadeer
Session 6, 12.00-13.00
AUTOMATIC INFERENCE OF STATIONARY FIELDS: A GENERALIZATION OF JAVA'S
FINAL FIELDS
Christopher Unkel and Monica S. Lam
DEMAND-DRIVEN ALIAS ANALYSIS FOR C
Xin Zheng and Radu Rugina
A THEORY OF PLATFORM-DEPENDENT LOW-LEVEL SOFTWARE
Marius Nita, Dan Grossman and Craig Chambers
Session 7, 14.30-15.30
GENERATING PRECISE AND CONCISE PROCEDURE SUMMARIES
Greta Yorsh, Eran Yahav and Satish Chandra
LIFTING ABSTRACT INTERPRETERS TO QUANTIFIED LOGICAL DOMAINS
Sumit Gulwani, Bill McCloskey and Ashish Tiwari
RELATIONAL INDUCTIVE SHAPE ANALYSIS
Bor-Yuh Evan Chang and Xavier Rival
Session 8, 16.00-17.00
A THEORY OF CONTRACTS FOR WEB SERVICES
Giuseppe Castagna, Nils Gesbert and Luca Padovani
MULTIPARTY ASYNCHRONOUS SESSION TYPES
Kohei Honda, Nobuko Yoshida and Marco Carbone
PC CHAIR'S REPORT AND MOST INFLUENTIAL POPL PAPER AWARD FOR 1998
Saturday January 12
Invited talk, 9.00-10.00
Session 9, 10.30-11.30
CLOWNS TO THE LEFT OF ME, JOKERS TO THE RIGHT (PEARL)
Conor McBride
FOUNDATIONS FOR STRUCTURED PROGRAMMING WITH GADTS
Patricia Johann and Neil Ghani
IMPERATIVE SELF-ADJUSTING COMPUTATION
Umut Acar, Amal Ahmed and Matthias Blume
Session 10, 12.00-13.00
CRYPTOGRAPHICALLY SOUND IMPLEMENTATIONS FOR TYPED INFORMATION-FLOW
SECURITY
Cedric Fournet and Tamara Rezk
ON THE COMPUTATIONAL SOUNDNESS OF CRYPTOGRAPHICALLY MASKED FLOWS
Peeter Laud
EXTENSIBLE SUBTYPING ENCODING
Hamed Alavi, Seth Gilbert and Rachid Guerraoui
Session 11, 14.30-15.30
FOCUSING AND HIGHER-ORDER ABSTRACT SYNTAX
Noam Zeilberger
A TYPE-THEORETIC FOUNDATION FOR PROGRAMMING WITH HIGHER-ORDER ABSTRACT
SYNTAX AND FIRST-CLASS SUBSTITUTIONS
Brigitte Pientka
AN APPROACH TO CALL-BY-NAME DELIMITED CONTINUATIONS
Hugo Herbelin and Silvia Ghilezan
Session 12, 16.00-17.00
THE DESIGN AND IMPLEMENTATION OF TYPED SCHEME
Sam Tobin-Hochstadt and Matthias Felleisen
BOOMERANG: RESOURCEFUL LENSES FOR STRING DATA
Aaron Bohannon, J. Nathan Foster, Benjamin C. Pierce, Alexandre
Pilkiewicz and Alan Schmitt
FROM DIRT TO SHOVELS: FULLY AUTOMATIC TOOL GENERATION FROM AD HOC DATA
Kathleen Fisher, David Walker, Kenny Zhu and Peter White