**************************************************************
* 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. [email protected] Program Chair: --------------------------- Michael Hicks Department of Computer Science University of Maryland, College Park, MD 20866, USA [email protected] 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 _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users
