* ACM SIGPLAN-SIGACT Symposium
* on
* Principles of Programming Languages
*
* January 25-27, 2012
* Philadelphia, PA, USA
*
* Call for Participation
*
*http://www.cse.psu.edu/popl/12/
***************************************************************
Important dates
------------------------
* Hotel reservation deadline: December 24, 2011
* Early registration deadline: December 24, 2011
* Conference: January 25-27, 2012
* Colocated events: January 22-29, 2012
Registration
--------------------------
To register online, please go to
https://regmaster3.com/2012conf/POPL12/register.php
The early registration deadline is December 24, 2011.
Hotel
-------------------------
All the conference events will take place at the Sheraton Society Hill
Hotel in Philadelphia's historic district. 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/12/
To be eligible for the special conference rate, bookings must be made
by December 24, 2011. 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.
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.
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/12/program.html
Program Highlights
-------------------------
Invited talks:
* Sir Charles Antony Richard Hoare, FRS, FREng, FBCS, Microsoft
Research
ACM SIGPLAN Programming Languages Achievement Award Interview
* J Strother Moore, University of Texas at Austin
Meta-Level Features in an Industrial-Strength Theorem Prover
* Jennifer Rexford, Princeton University
Programming Languages for Programmable Networks
Other attractions
-------------------------
POPL TutorialFest!:
POPL 2012 will have a TutorialFest! event with seven "distilled" 90
minute tutorials. This event is on January 28, immediately following
the main POPL conference. The TutorialFest! requires separate
registration and registrants of TutorialFest! may attend any of the
tutorials offered throughout the day.
More information on the TutorialFest! is available at:
http://www.cse.psu.edu/popl/12/tutorial.html
Affiliated Events
--------------------------
* POPL TutorialFest: January 28, 2012
* VMCAI:Verification Model Checking and Abstract Interpretation
* January 22-24, 2012
http://lara.epfl.ch/vmcai2012/
* LADA: Languages for Distributed Algorithms
* January 23-24, 2012
http://sites.google.com/site/ladameeting/
* PADL: Practical Applications of Declarative Languages
* January 23-24, 2012
http://research.microsoft.com/en-us/um/people/crusso/padl12/
* PEPM: Partial Evaluation and Semantics-Based Program Manipulation
* January 23-24, 2012
http://www.program-transformation.org/PEPM12
* PLMW: The CRA-W/CDC and SIGPLAN Programming Languages Mentoring
Workshop
* January 24, 2012
http://www.cis.upenn.edu/~sweirich/plmw12/
* PLPV: Programming Languages meets Program Verification
* January 24, 2012
http://research.microsoft.com/en-us/um/people/nswamy/plpv12/
* DAMP: Declarative Aspects of Multicore Programming
* January 28, 2012
http://www.mpi-sws.org/~umut/damp2012/
* OBT: Off the Beaten Track: Underrepresented Problems for Programming
Language Researchers
* January 28, 2012
http://www.cs.princeton.edu/~dpw/obt/
* TLDI:Types in Language Design and Implementation
* January 28, 2012
http://www.cis.upenn.edu/~bcpierce/tldi12/
* VSTTE: Verified Software: Theories, Tools and Experiments
* January 28-29, 2012
https://sites.google.com/site/vstte2012/
Travel awards and visa support letters
--------------------------------
A limited number of grants are available through the SIGPLAN
Professional Activities Committee (PAC) to support students going to
POPL. You must be an ACM member to apply.
Students that are interested in attending both POPL and the PLMW
Workshop should first seek funds via PLMW and then contact PAC if the
PLMW grant is not awarded. PLMW grants are explained on the PLMW
website.
Requests for visa support letters for purposes of attending or
presenting at POPL 2012 are handled by ACM. More information is
available on the POPL 2012 website.
Program
---------------------------
Wednesday, January 25
===========================
* 8:30-9:20: Breakfast
* 9:20-9:30: Welcome
* 9:30-10:30: Invited Talk (Session chairs: Andrew P. Black, Peter
O'Hearn)
- SIGPLAN Distinguished Achievement Award Presentation and Interview
Tony Hoare, Microsoft Research.
* 10:30-11:00: Break
* 11:00-12:30: Session on Verification (Chair: Ranjit Jhala):
-Freefinement (Stephan van Staden, Cristiano Calcagno, and Bertrand
Meyer)
- Underspecified harnesses and interleaved bugs (Saurabh Joshi,
Shuvendu Lahiri, and Akash Lal)
- A Program Logic for JavaScript (Philippa Gardner, Sergio Maffeis,
and Gareth Smith)
* 11:00-12:30: Session on Semantics (Chair: Patricia Johann):
- Higher-Order Functional Reactive Programming in Bounded Space
(Neelakantan R Krishnaswami and Nick Benton and Jan Hoffmann)
- The Marriage of Bisimulations and Kripke Logical Relations
(Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis)
- Information Effects (Roshan James and Amr Sabry)
* 12:30-2:00: Lunch
* 2:00-3:30: Session on Privacy and Access Control (Chair: Nikhil
Swamy):
- A Language for Automatically Enforcing Privacy Policies (Jean Yang,
Kuat Yessenov, and Armando Solar-Lezama)
- Probabilistic Relational Reasoning for Differential Privacy (Gilles
Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Beguelin)
- Access Permission Contracts for Scripting Languages (Phillip
Heidegger, Annette Bieniusa, and Peter Thiemann)
* 2:00-3:30: Session on Decision Procedures (Chair: Swarat Chaudhuri):
- Recursive Proofs for Inductive Tree Data-Structures (P Madhusudan,
Xiaokang Qiu, and Andrei Stefanescu)
- Symbolic Finite State Transducers, Algorithms and Applications
(Nikolaj Bjorner, Pieter Hooimeijer, and Benjamin Livshits, David
Molnar, and Margus Veanes)
- Constraints as Control (Ali Sinan Köksal, Viktor Kuncak, and
Philippe Suter)
* 3:30-4:15: Break
* 4:15-5:15: Session on Security (Chair: Neelakantan Krishnaswami):
- Multiple Facets for Dynamic Information Flow (Thomas Austin and
Cormac Flanagan)
- Defining Code-injection Attacks (Donald Ray and Jay Ligatti)
* 4:15-5:15: Session on Complexity for Concurrency (Chair: P.
Madhusudan):
- Deciding Choreography Realizability (Samik Basu, Tevfik Bultan, and
Meriem Ouederni)
- Analysis of Recursively Parallel Programs (Ahmed Bouajjani and
Michael Emmi)
* 5:15-6:00: Break
* 6:00-8:00: Student Session (Chair: Tobias Wrigstad)
Thursday, January 26
===========================
* 8:30-9:20: Breakfast
* 9:20-9:30: Announcements
* 9:30-10:30: Invited Talk (Session chair: Michael Hicks)
- Programming Languages for Programmable Networks
Jennifer Rexford, Princeton University
* 10:30-11:00: Break
* 11:00-12:30: Session on Medley (Chair: Suresh Jagannathan):
- A Compiler and Run-time System for Network Programming Languages
(Christopher Monsanto, Nate Foster, Rob Harrison, and David Walker)
- Nested Refinements: A Logic For Duck Typing (Ravi Chugh, Patrick M
Rondon, and Ranjit Jhala)
- An Abstract Interpretation Framework for Termination. (Patrick
Cousot and Radhia Cousot)
* 11:00-12:30: Session on Mechanized Proofs (Chair: Adam Chlipala):
- Playing in the Grey Area of Proofs (Krystof Hoder, Laura Kovacs, and
Andrei Voronkov)
- Static and User-Extensible Proof Checking (Antonis Stampoulis and
Zhong Shao)
- Run Your Research: On the Effectiveness of Lightweight Mechanization
(Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, and
Matthias Felleisen, Matthew Flatt, Jay McCarthy, Jon Rafkind, Sam
Tobin-Hochstadt, and Robert Bruce Findler)
* 12:30-2:00: Lunch
* 2:00-3:30: Session on Concurrency (Chair: Matt Parkinson):
- Verification of Parameterized Concurrent Programs By Modular
Reasoning about Data and Control (Azadeh Farzan and Zachary Kincaid)
-Resource-Sensitive Synchronization Inference by Abduction (Matko
Botincan and Mike Dodds and Suresh Jagannathan)
- Syntactic Control of Interference for Separation Logic (Uday S Reddy
and John C Reynolds)
* 2:00-3:30: Session on Type Theory (Chair: Stephanie Weirich):
- Canonicity for 2-Dimensional Type Theory (Daniel R Licata and Robert
Harper)
- Algebraic Foundations for Effect-Dependent Optimisations (Ohad
Kammar and Gordon Plotkin)
- On the Power of Coercion Abstraction (Didier Remy and Julien Cretin)
* 3:30-4:15: Break
* 4:15-5:15: Session on Dynamic Analysis (Chair: Aarti Gupta):
- Abstractions From Tests (Mayur Naik, Hongseok Yang, and Ghila
Castelnuovo and Mooly Sagiv)
- Sound Predictive Race Detection in Polynomial Time (Yannis
Smaragdakis, Jacob M Evans, and Caitlin Sadowski, Jaeheon Yi, and
Cormac Flanagan)
* 4:15-5:15: Session on Names and Binders (Chair: Zhong Shao):
- Towards Nominal Computation (Mikolaj Bojanczyk, Laurent Braud,
Bartek Klin, and Slawomir Lasota)
- Programming with Binders and Indexed Data-Types (Andrew Cave and
Brigitte Pientka)
* 5:15-5:45: Business meeting
* 7:00-: Banquet
Friday, January 27
===========================
* 8:30-9:20: Breakfast
* 9:20-9:30: POPL 2013 preview
* 9:30-10:30: Invited Talk (Session chair: John Field)
- Meta-level Features in an Industrial-Strength Theorem Prover
J Strother Moore, University of Texas
* 10:30-11:00: Break
* 11:00-12:30: Session on Verified Transformations (Chair: Chris
Hawblitzel):
- Formalizing the LLVM Intermediate Representation for Verified
Program Transformation (Jianzhou Zhao, Steve Zdancewic, Santosh
Nagarakatte, and Milo M K Martin)
- Optimal Randomized Transformation of Approximate Computations
(Zeyuan Allen Zhu, Sasa Misailovic, Jonathan Kelner, and Martin
Rinard)
- A Rely-Guarantee-Based Simulation for Verifying Concurrent Program
Transformations (Hongjin Liang, Xinyu Feng, and Ming Fu)
* 11:00-12:30: Session on Functional Programming (Chair: Dimitrios
Vytiniotis):
- A Unified Approach to Fully Lazy Sharing (Thibaut Balabonski)
- The Ins and Outs of Gradual Type Inference (Aseem Rastogi and Avik
Chaudhuri and Basil Hosmer)
- Edit Lenses (Martin Hofmann and Benjamin C Pierce and Daniel Wagner)
* 12:30-2:00: Lunch
* 2:00-3:30: Session on C/C++ Semantics (Chair: Andreas Podelski):
- Clarifying and compiling C/C++ concurrency: from C++0x to POWER
(Mark Batty, Kayvan Memarian, and Scott Owens, Susmit Sarkar, and
Peter Sewell)
- A mechanized semantics for C++ object construction and destruction,
with applications to resource management (Tahina Ramananandro, Gabriel
Dos Reis, and Xavier Leroy)
- An Executable Formal Semantics of C with Applications (Chucky
Ellison and Grigore Rosu)
* 2:00-3:30: Session on Type Systems (Chair: Norman Ramsey):
- A Type Theory for Probability Density Functions (Sooraj Bhat, Ashish
Agarwal, and Richard Vuduc and Alexander Gray)
- A Type System for Borrowing Permissions (Karl Naden, Robert L
Bocchino Jr, Kevin Bierhoff, and Jonathan Aldrich)
- Self-Certification: Bootstrapping Certified Typecheckers in F* with
Coq (Pierre-Yves Strub and Nikhil Swamy, Cedric Fournet, and Juan
Chen)
* 3:30-4:00: Closing and Raffle
General Chair:
--------------------------
John Field
Google
76 Ninth Avenue,
New York, NY 10011, USA.
jfield@google.com
Program Chair:
---------------------------
Michael Hicks
Department of Computer Science
University of Maryland,
College Park, MD 20866, USA
mwh@cs.umd.edu
Program Committee:
---------------------------
Swarat Chaudhuri, Rice University, USA
Adam Chlipala, MIT, USA
Dan R. Ghica, University of Birmingham, UK
Aarti Gupta, NEC Labs America, USA
Chris Hawblitzel, Microsoft Research, Redmond, USA
Suresh Jagannathan, Purdue University, USA
Ranjit Jhala, University of California, San Diego, USA
Sorin Lerner, University of California, San Diego, USA
Ondrej Lhotak, University of Waterloo, Canada
P. Madhusudan, University of Illinois, Urbana-Champaign, USA
Rupak Majumdar, MPI-SWS, Germany
Matthew Might, University of Utah, USA
Todd Millstein, University of California, Los Angeles, USA
Greg Morrisett, Harvard University, USA
Andrew Myers, Cornell University, USA
Matthew Parkinson, Microsoft Research, Cambridge, UK
Frank Piessens, K.U. Leuven, Belgium
Andrew Pitts, University of Cambridge, UK
Andreas Podelski, University of Freiburg, Germany
François Pottier, INRIA, France
Norman Ramsey, Tufts University, USA
Tachio Terauchi, Nagoya University, Japan
Mandana Vaziri, IBM Research, USA
Dimitrios Vytiniotis, Microsoft Research, Cambridge, UK
Nobuko Yoshida, Imperial College, London, UK
Francesco Zappa Nardelli, INRIA, France
Posts
