[racket] POPL 2011: Call for participation
**************************************************************
* ACM SIGPLAN-SIGACT Symposium
* on
* Principles of Programming Languages
*
* January 26-28, 2011
* Austin, TX, USA
* Call for Participation
*
* http://www.cse.psu.edu/popl/11/
***************************************************************
Important dates
------------------------
* Deadline for student travel grant
applications for full consideration: December 17, 2010
* Hotel reservation deadline: December 21, 2010
* Early registration deadline: December 31, 2010
* Conference: January 26-28, 2011
Scope
-------------------------
The annual Symposium on Principles of Programming Languages is a
forum for the discussion of fundamental principles and important
innovations in the design, definition, analysis, transformation,
implementation and verification of programming languages, programming
systems, and programming abstractions. Both experimental and
theoretical papers are welcome.
Hotel
-------------------------
All the conference events will take place at the Omni Austin Hotel
in downtown Austin, TX. We encourage attendees to stay at the conference
hotel. Information about the hotel can be found on the POPL web page:
http://www.cse.psu.edu/popl/11/
To be eligible for the special conference rate, bookings must be made
by ** December 21, 2010 **. However, as the conference rate applies only to
a limited number of rooms, attendees are encouraged to make their
hotel reservations at the earliest opportunity.
Registration
--------------------------
To register online, please go to
https://regmaster3.com/2011conf/POPL11/register.php
The early registration deadline is ** December 31, 2010 **.
This year, we are capping the registration for POPL at 300 in order to
provide an optimal conference experience at the Omni Hotel.
Therefore, please register early.
Student Attendees
--------------------------
The SIGPLAN Professional Activities Committee (PAC) awards travel
grants that are typically reserved for students presenting papers or
posters at conferences. In addition to the SIGPLAN PAC grants, we are
pleased to announce the availability of a limited number of travel awards,
though a grant from the National Science Foundation, for students who
want to attend the conference but are not presenting.
If you are a student interested in learning more about state of the art
research in programming language principles, please consider applying
for a POPL 2011 travel award. More information about student travel grants
are available at the conference homepage.
This student travel grant program is designed specifically to encourage
participation from junior students and underrepresented groups.
Preliminary program
--------------------------
A preliminary program can be found at the end of this email in text
format, or it can be found here:
http://www.cse.psu.edu/popl/11/program.html
Program Highlights
-------------------------
Invited talks:
* Xavier Leroy (INRIA). "Verified squared: does critical software
deserve verified tools?"
* Matthew MacLaurin (Microsoft). "The Design of Kodu: A Tiny
Visual Programming Language for Children on the Xbox 360."
* Talks In memory of Robin Milner. Organized by Andrew Gordon
(Microsoft) and Peter Sewell (Cambridge).
Speakers: Robert Harper (CMU), Alan Jeffrey (Bell Labs), and
John Harrison (Intel).
Other attractions
-------------------------
POPL Games and Jazz Dinner:
The POPL dinner will be at the conference hotel on the evening of
Wednesday January 26. It will feature live Jazz music and Xbox/Kinect
gaming. Three Kinect-enabled Xboxes, ready to play, will be available
before and after the POPL dinner.
POPL Xbox 360 Raffle
We will give away the three Xbox 360 4GB Console with Kinect bundles
in a raffle at the very end of the conference. Your POPL registration enters
you in the raffle. You must be present to win.
General Chair:
--------------------------
Thomas Ball
Microsoft Research
One Microsoft Way, Redmond, WA 98052, USA.
tball at microsoft.com
Program Chair:
---------------------------
Mooly Sagiv
Schreiber 317, School of Computer Science
Tel-Aviv University, Tel-Aviv 69978, Israel
msagiv at post.tau.ac.il
Program Committee:
---------------------------
Radhia Cousot Ecole Normale Supérieure
Oege de Moor Oxford University Computing Laboratory
Derek Dreyer MPI-SWS
Azadeh Farzan University of Toronto
Kathleen Fisher AT&T Laboratories
Matthew Fluet Rochester Institute of Technology
Jeff Foster University of Maryland
Stephen Freund Williams College
Philippa Gardner Imperial College, London
Dan Grossman University of Washington
Sumit Gulwani Microsoft Research
Tim Harris Microsoft Research
Naoki Kobayashi Tohoku University
Viktor Kuncak EPFL
Ken McMillan Cadence Research Laboratories
Anders Moeller Aarhus University
Peter Muller ETH Zurich
Aleks Nanevski IMDEA Software
David Naumann Stevens Institute of Technology
Prakash Panangaden McGill University
G. Ramalingam Microsoft Research
Jan Vitek Purdue University
Eran Yahav IBM Research
Hongseok Yang Queen Mary, University of London
Steve Zdancewic University of Pennsylvania
Affiliated Events
--------------------------
* DAMP: Declarative Aspects of Multicore Programming
* January 23, 2011
* Nominal: Tutorial on Using Nominal Isabelle for PL Research
* January 23, 2011
* PLPV: Programming Languages meets Program Verification
* January 29, 2011
* PADL: Practical Applications of Declarative Languages
* January 24-25, 2011
* PEPM: Partial Evaluation and Semantics-Based Program Manipulation
* January 24-25, 2011
* STOP: Workshop on Script to Program Evolution
* January 29, 2011
* TLDI:Types in Language Design and Implementation
* January 25, 2011
* TPTPA: Tutorial on Theorem Proving Tools for Program Analysis
* January 24-25, 2011
* Verico: Verification of Concurrent Data Structures
* January 29, 2011
* VMCAI:Verification Model Checking and Abstract Interpretation
* January 23-25, 2011
Preliminary Program
---------------------------
Wednesday, January 26
===========================
* 8:45-9:00: Welcome (Tom Ball, Mooly Sagiv)
* 9:00-10:00: Invited Talk
- "Verified squared: does critical software deserve verified tools?"
Xavier Leroy, INRIA.
* 10:00-10:30: Break
* 10:30-12:00: Session on Pointer Analysis:
- "Points-To Analysis with Efficient Strong Updates." O. Lhotak, K. Chung
- "Pick Your Contexts Well: Understanding Object-Sensitivity (The Making of
a Precise and Scalable Pointer Analysis)." Y. Smaragdakis, M. Bravenboer,
O. Lhotak
- "Learning Minimal Abstractions." P. Liang, O. Tripp, M. Naik
* 10:30-12:00: Session on Semi-Automated Verification:
- "Relaxed-Memory Concurrency and Verified Compilation." J. Sevcik,
V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, P. Sewell.
- "Mathematizing C++ Concurrency." M. Batty, S. Owens, S. Sarkar, P.
Sewell, T. Weber
- "Formal verification of object layout for C++ multiple inheritance."
T. Ramananandro, G. Reis, X. Leroy
* 12:00-1:30: Lunch
* 1:30-3:00: Session on Static Analysis:
- "Static Analysis for Multi-Staged Programs via Unstaging Translation."
W. Choi, B. Aktemur, K. Yi, M. Tatsuta
- "Static analysis of interrupt-driven programs." M. Schwarz, H.
Seidl, V. Vojdani, M. Muller-Olm, P. Lammich
- "A Parametric Segmentation Functor for Fully Automatic and Scalable
Array Content Analysis." P. Cousot, R. Cousot, F. Logozzo
* 1:30-3:00: Session on Semantic Models and Translations:
- "Step-Indexed Kripke Models over Recursive Worlds." L. Birkedal, B. Reus,
J. Schwinghammer, K. Stovring, J. Thamsborg, H. Yang
- "A Kripke Logical Relation Between ML and Assembly." C. Hur, D. Dreyer
- "A typed store-passing translation for general references." F. Pottier
* 3:00-3:30: Break
* 3:30-5:00: Session on Shape Analysis:
- "A Shape Analysis for Optimizing Parallel Graph Programs."
D. Prountzos, R. Manevich, K. Pingali, K. McKinley
- "Calling Context Abstraction with Shapes." X. Rival, B. Chang
- "Precise Reasoning for Programs Using Containers." I. Dillig, T.
Dillig, A. Aiken
* 3:30-5:00: Session on Type Abstractions:
- "Blame for All." A. Ahmed, R. Findler, J. Siek, P. Wadler
- "Correct Blame for Contracts: No More Scapegoating." C. Dimoulas, R.
Findler, C. Flanagan, M. Felleisen
- "Generative type abstraction and type-level computation." S. Weirich,
D. Vytiniotis, S. Peyton-Jones, S. Zdancewic
* 5:00-7:00: Free time
* 7:00-8:00: Appetizers, Drinks, and Xbox/Kinect/Kodu Game Room
* 8:00-9:30: Buffet Dinner and Jazz
* 9:30-11:00: Xbox/Kinect/Kodu Game Room
Thursday, January 27
===========================
* 9:00-10:00: Invited Talk
- "The Design of Kodu: A Tiny Visual Programming Language for Children
on the Xbox 360."
Matthew MacLaurin, Microsoft
* 10:00-10:30: Break
* 10:30-12:00: Session on Separation Logic:
- "A separation logic for refining concurrent objects." A. Turon, M. Wand
- "Modular Reasoning for Deterministic Parallelism." M. Dodds,
S. Jagannathan, M. Parkinson
- "Expressive Modular Fine-Grained Concurrency Specifications."
B. Jacobs, F. Piessens
* 10:30-12:00: Session on Automata:
- "The Tree Width of Auxiliary Storage." P. Madhusudan, G. Parlato
- "Fresh-Register Automata." N. Tzevelekos
- "Vector Addition System Reachability Problem In Less Than 7 Pages." J.
Leroux
* 12:00-1:30: Lunch
* 1:30-3:00: Session on Synthesis:
- "Automating String Processing in Spreadsheets using Input-Output
Examples."
S. Gulwani
- "Constraint Based Inference of Auxiliary Variables and
Relies/Guarantees for Verifying Multi-Threaded Programs." A. Gupta, C.
Popeea,
A. Rybalchenko
- "Geometry of Synthesis III: Resource management through type inference."
D. Ghica, A. Smith
* 1:30-3:00: Session on Algebra:
- "Multivariate Amortized Resource Analysis." J. Hoffmann, K. Aehlig, M.
Hofmann
- "Elements of Symmetric Lenses." M. Hofmann, B. Pierce, D. Wagner
- "Regular Expression Containment: Coinductive Axiomatization and
Computational Interpretation." F. Henglein, L. Nielsen
* 3:00-3:30: Break
* 3:30-5:00: Session on Model Checking:
- "Making Prophecies with Decision Predicates." B. Cook, E. Koskinen
- "Delay-bounded scheduling." M. Emmi, S. Qadeer, Z. Rakamaric
- "On Interference Abstractions." N. Sinha, C. Wang
* 3:30-5:00: Session on Types:
- "Dynamic Multirole Session Types." P. Denielou, N. Yoshida
- "Practical Affine Types." J. Tov, R. Pucella
- "Dynamic Inference of Static Types for Ruby." J. An, A. Chaudhuri,
J. Foster, M. Hicks
* 5:00-5:15: Break
* 5:15-6:15: Business Session
* 6:15-8:00: Break
* 8:00-10:00: Student Presentation Session
Friday, January 28
===========================
* 9:00-10:00: Invited Talk
- "Robin Milner: Verification, Languages, and Concurrency"
Andrew D. Gordon (Microsoft), Peter Sewell (Cambridge), Robert Harper
(CMU),
Alan Jeffrey (Bell Labs), John Harrison (Intel)
* 10:00-10:30: Break
* 10:30-12:00: Session on Complexity:
- "Space Overhead Bounds for Dynamic Memory Management with Partial
Compaction."
A. Bendersky, E. Petrank
- "Laws of Order: Expensive Synchronization in Concurrent Algorithms
Cannot be Eliminated."
H. Attiya, R. Guerraoui, D. Hendler, P. Kuznetsov, M. Michael, M. Vechev
- "Complexity of Pattern-based Verification for Multithreaded Programs."
J. Esparza, P. Ganty
* 10:30-12:00: Medley Session:
- "EigenCFA: Accelerating flow analysis with GPUs." T. Prabhu, S.
Ramalingam, M. Might, M. Ha
- "Bisimulation for quantum processes." Y. Feng, R. Duan, M. Ying
- "Safe Nondeterminism in a Deterministic-by-Default Parallel
Language." R. Bocchino,
S. Heumann, N. Honarmand, S. Adve, V. Adve, A. Welc, T. Shpeisman
* 12:00-1:30: Lunch
* 1:30-3:00: Session on Compilation:
- "Loop Transformations: Convexity, Pruning and Optimization." L.
Pouchet, U. Bondhugula,
C. Bastoul, A. Cohen, J. Ramanujam, P. Sadayappan, N. Vasilache
- "The Essence of Compiling with Traces." S. Guo, J. Palsberg
- "Resourceable, Retargetable, Modular Instruction Selection Using a
Machine-Independent,
Type-Based Tiling of Low-Level Intermediate Code." N. Ramsey, J. Dias
* 1:30-3:00: Session on Verification:
- "Verifying Higher-Order Programs with Pattern-Matching Algebraic Data
Types." C. Ong, S. Ramsay
- "Streaming Transducers for Algorithmic Verification of Single-Pass List
Processing Programs." R. Alur, P. Cerny
- "Decidable logics combining heap structures and data." P.
Madhusudan, G. Parlato, X. Qiu
* 3:00-3:30: Break
* 3:30-4:00:
- "A Technique for the Effective and Automatic Reuse of Classical
Compiler Optimizations on Multithreaded Code."
P. G. Joisha, R. S. Schreiber, P. Banerjee, Hans-J. Boehm
* 4:00-4:15: Wrap-up and Xbox/Kinect Raffle Drawing