 |
POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesTata Institute of Fundamental Research, Mumbai, India
|
POPL 2015 PROGRAM - Overview
| Mon 12 Jan |
Tue 13 Jan |
Wed 14 Jan |
Thu 15 Jan |
Fri 16 Jan |
Sat 17 Jan |
Sun 18 Jan |
| VMCAI | POPL | CoqPL | ||||
| PLVNET | CPP | OBT | ||||
| PEPM | WEPL | |||||
| Tutorials | PLMW | |||||
WEDNESDAY 14 January (DAY 0)
17:30 - 21:30 Workshop dinner (open to all workshop participants)
THURSDAY 15 January (DAY 1)
9:10-9:20 Welcoming Remarks: Sriram Rajamani and David Walker
9:20-9:30 Milner Award
9:30-10:30 Keynote address (HBA, Chair: Sriram Rajamani, Microsoft Research)
Automating Repetitive Tasks for the Masses
Sumit Gulwani
10:30-11:00 Break
11:00-12:30 6 papers, dual track
Session 1A: Types I (HBA, Chair: Jeremy Gibbons, Oxford University)
Functors are Type Refinement Systems
Paul-André Melliès (CNRS, Université Paris Diderot)
Noam Zeilberger (MSR-Inria)
Integrating Linear and Dependent Types
Neel Krishnaswami (University of Birmingham)
Pierre Pradic (ENS Lyon)
Nick Benton (Microsoft Research)
Higher Inductive Types as Homotopy-Initial Algebras
Kristina Sojakova (Carnegie Mellon University)
Session 1B: Security (AG66, Chair: Karthikeyan Bhargavan, Inria)
Runtime Enforcement of Security Policies on Black Box Reactive Programs
Minh Ngo (University of Trento)
Fabio Massacci (University of Trento)
Dimiter Milushev (KU Leuven)
Frank Piessens (KU Leuven)
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
Gilles Barthe (IMDEA Software Institute)
Marco Gaboardi (University of Dundee)
Emilio Gallego Arias (University of Pennsylvania)
Justin Hsu (University of Pennsylvania)
Aaron Roth (University of Pennsylvania)
Pierre-Yves Strub (IMDEA Software Institute)
Differential Privacy: Now it's Getting Personal
Hamid Ebadi (Chalmers University of Technology)
David Sands (Chalmers University of Technology)
Gerardo Schneider (Chalmers University of Technology)
12:30-2:00 Lunch
2:00-3:30 6 papers, dual track
Session 2A: Program Analysis I (HBA, Chair: Raghavan Komondoor, IISc Bangalore)
Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks
Hao Tang (Peking University, China)
Xiaoyin Wang (University of Texas at San Antonio)
Lingming Zhang (University of Texas at Dallas)
Bing Xie (Peking University, China)
Lu Zhang (Peking University, China)
Hong Mei (Peking University, China)
Faster Algorithms for Algebraic Path Properties in RSMs with Constant Treewidth
Krishnendu Chatterjee (IST Austria)
Prateesh Goyal (IIT Bombay)
Rasmus Ibsen-Jensen (IST Austria)
Andreas Pavlogiannis (IST Austria)
Predicting Program Properties from "Big Code"
Veselin Raychev (ETH Zurich)
Martin Vechev (ETH Zurich)
Andreas Krause (ETH Zurich)
Session 2B: Domain-specific Languages (AG66, Chair: Stephanie Weirich, University of Pennsylvania)
DReX: A Declarative Language for Efficiently Computable Regular String Transformations
Rajeev Alur (University of Pennsylvania)
Loris D'Antoni (University of Pennsylvania)
Mukund Raghothaman (University of Pennsylvania)
Data Parallel String Manipulating Programs
Margus Veanes (Microsoft Research)
Todd Mytkowicz (Microsoft Research)
David Molnar (Microsoft Research)
Ben Livshits (Microsoft Research)
Ur/Web: A Simple Model for Programming the Web
Adam Chlipala (MIT CSAIL)
3:30-4:00 Break
4:00-5:30 6 papers, dual track
Session 3A: Dynamic Verification (HBA, Chair: Jan Vitek, Northeastern University)
Safe and Efficient Gradual Typing for TypeScript
Aseem Rastogi (University of Maryland, College Park)
Nikhil Swamy (Microsoft Research)
Cedric Fournet (Microsoft Research)
Gavin Bierman (Oracle Labs)
Panagiotis Vekris (University of California, San Diego)
Space-Efficient Manifest Contracts
Michael Greenberg (Princeton University)
Manifest Contracts for Datatypes
Taro Sekiyama (Kyoto University)
Yuki Nishida (Kyoto University)
Atsushi Igarashi (Kyoto University)
Session 3B: Concurrency I (AG66, Mooly Sagiv, Tel Aviv University)
Common Compiler Optimisations are Invalid in the C11 Memory Model and What We Can Do About It
Viktor Vafeiadis (MPI-SWS)
Thibaut Balabonski (INRIA)
Soham Chakraborty (MPI-SWS)
Robin Morisset (INRIA)
Francesco Zappa Nardelli (INRIA)
From Communicating Machines to Graphical Choreographies
Julien Lange (Imperial Colllege London)
Emilio Tuosto (University of Leicester)
Nobuko Yoshida (Imperial Colllege London)
A Scalable, Correct Time-Stamped Stack
Mike Dodds (University of York)
Andreas Haas (University of Salzburg)
Christoph M. Kirsch (University of Salzburg)
5:30-6:30 Poster session (Foyer) and SIGPLAN business meeting (AG66) (in parallel)
6:30-7:30 Cultural program (HBA)
7:30-10:30 Dinner at TIFR lawns
FRIDAY 16 January (DAY 2)
6:00-6:30 Morning 5k run at Marine Drive
9:00-10:30 6 papers, dual track
Session 4A: Compiler Correctness (HBA, Chair: Adam Chlipala, MIT)
Formal Verification of a C Static Analyzer
Jacques-Henri Jourdan (Inria Paris-Rocquencourt)
Vincent Laporte (IRISA and U. Rennes 1)
Sandrine Blazy (IRISA and U. Rennes 1)
Xavier Leroy (Inria Paris-Rocquencourt)
David Pichardie (IRISA and ENS Rennes)
Analyzing Program Analyses
Roberto Giacobazzi (University of Verona)
Francesco Logozzo (Microsoft Research)
Francesco Ranzato (University of Padova)
Compositional CompCert
Gordon Stewart (Princeton University)
Lennart Beringer (Princeton University)
Santiago Cuellar (Princeton University)
Andrew W. Appel (Princeton University)
Session 4B: Types II (AG66, Chair: Deepak Garg, MPI-SWS)
Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction
Giuseppe Castagna (CNRS - Université Paris Diderot)
Kim Nguyen (LRI - Université Paris Sud)
Zhiwu Xu
Pietro Abate (Université Paris Diderot)
Principal Type Schemes for Gradual Programs
Ronald Garcia (University of British Columbia)
Matteo Cimini (Indiana University)
Dependent Information Flow Types
Luísa Lourenço (CITI and NOVA-LINCS / Universidade Nova de Lisboa)
Luís Caires (CITI and NOVA-LINCS / Universidade Nova de Lisboa)
10:30-11:00 Break
11:00-12:30 6 papers dual track
Session 5A: Regular Languages and Automata (HBA, Chair: Supratik Chakraborty, IIT Bombay)
Abstract Symbolic Automata
Mila Dalla Preda (University of Verona)
Roberto Giacobazzi (University of Verona)
Arun Lakhotia (University of Louisiana)
Isabella Mastroeni (University of Verona)
A Coalgebraic Decision Procedure for NetKAT
Nate Foster (Cornell University)
Dexter Kozen (Cornell University)
Matthew Milano (Cornell University)
Alexandra Silva (Raboud University Nijmegen)
Laure Thompson (Cornell University)
Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
Damien Pous (CNRS, France)
Session 5B: Programming Models I (AG66, Chair: Frank Pfenning, CMU)
Programming up to Congruence
Vilhelm Sjöberg (University of Pennsylvania)
Stephanie Weirich (University of Pennsylvania)
A Meta Lambda Calculus with Cross-Level Computation
Kazunori Tobisawa (Graduate School of Mathematical Sciences, The University of Tokyo)
Algebraic Effects, Linearity, and Quantum Programming Languages
Sam Staton (Radboud University Nijmegen)
12:30-2:00 Lunch
2:00-3:30 6 papers dual track
Session 6A: Concurrency II (HBA, Chair: Nishant Sinha, IBM Research India)
Proof Spaces for Unbounded Parallelism
Azadeh Farzan (University of Toronto)
Zachary Kincaid (University of Toronto)
Andreas Podelski (University of Freiburg)
Equations, Contractions, and Unique Solutions
Davide Sangiorgi (University of Bologna and INRIA)
Succinct Representation of Concurrent Trace Sets
Ashutosh Gupta (IST Austria)
Thomas A. Henzinger (IST Austria)
Arjun Radhakrishna (IST Austria)
Roopsha Samanta (IST Austria)
Thorsten Tarrach (IST Austria)
Session 6B: Semantics (AG66, Chair: Arjun Guha, University of Massachusetts, Amherst)
K-Java: A Complete Semantics of Java
Denis Bogdanas (Alexandru Ioan Cuza University Iasi, Romania)
Grigore Rosu (University of Illinois at Urbana-Champaign)
Towards the Essence of Hygiene
Michael D. Adams (University of Utah, University of Illinois at Urbana/Champaign)
Self-Representation in Girard's System U
Matt Brown (UCLA)
Jens Palsberg (UCLA)
3:30-4:00 Break
4:00-5:00 Keynote address (HBA, Chair: David Walker, Priceton University)
Coding by Everyone, Every Day
Peter Lee
5:00-5:30 POPL'15 Report (HBA)
5:30-5:45 POPL'16 Preview (HBA)
6:30 Banquet & Announcement of the most influential paper from POPL 2005
SATURDAY 17 January (DAY 3)
9:00-10:00 Keynote address (HBA, Chair: Paritosh Pandya, TIFR)
Databases and Programming: Two Subjects Divided by a Common Language?
Peter Buneman
10:00-10:30 Break
10:30 -11:30 4 papers, dual track
Session 7A: Probabilistic Programs (HBA, Chair: S Akshay, IIT Bombay)
Probabilistic Termination
Luis Maria Ferrer Fioriti (Saarland University)
Holger Hermanns (Saarland University)
Leveraging Weighted Automata to Compositional Reasoning about Concurrent Probabilistic Systems
Fei He (Tsinghua University)
Xiaowei Gao (Tsinghua University)
Bow-Yaw Wang (Academia Sinica)
Lijun Zhang (Institute of Software, Chinese Academy of Sciences)
Session 7B: Programming Models II (AG66, Chair: Roberto Giacobazzi, University of Verona)
Full Abstraction for Signal Flow Graphs
Filippo Bonchi (Ecole Normale Supérieure Lyon; France)
Pawel Sobocinski (University of Southampton, UK)
Fabio Zanasi (Ecole Normale Supérieure Lyon; France
Conjugate Hylomorphisms: The Mother of All Structured Recursion Schemes
Ralf Hinze (University of Oxford)
Nicolas Wu (University of Oxford)
Jeremy Gibbons (University of Oxford)
11:30-12:30 Remembering Radhia Cousot, Susan Horwitz
12:30-2:00 Lunch
2:00-3:30 6 papers, dual track
Session 8A: Program Analysis II (HBA, Chair: Akash Lal, Microsoft Research)
Quantitative Interprocedural Analysis
Krishnendu Chatterjee (IST Austria)
Andreas Pavlogiannis (IST Austria)
Yaron Velner (Tel Aviv University)
Specification Inference Using Context-Free Language Reachability
Osbert Bastani (Stanford University)
Saswat Anand (Stanford University)
Alex Aiken (Stanford Univeristy)
On Characterizing the Data Access Complexity of Programs
Venmugil Elango (The Ohio State University)
Fabrice Rastello (Inria)
Louis-Noel Pouchet (University of California Los Angeles)
J. Ramanujam (Louisiana State University)
P. Sadayappan (The Ohio State University)
Session 8B: Verification (AG66, Chair: Sumit Gulwani, Microsoft Research)
Sound Modular Verification of C Code Executing in an Unverified Context
Pieter Agten (iMinds-DistriNet, KU Leuven)
Bart Jacobs (iMinds-DistriNet, KU Leuven)
Frank Piessens (iMinds-DistriNet, KU Leuven)
Deep Specifications and Certified Abstraction Layers
Ronghui Gu (Yale University)
Jeremie Koenig (Yale University)
Tahina Ramananandro (Yale University)
Zhong Shao (Yale University)
Newman Wu (Yale University)
Shu-chun Weng (Yale University)
Haozhong Zhang (University of Science and Technology of China)
Yu Guo (University of Science and Technology of China)
From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification
Adam Chlipala (MIT CSAIL)
3:30-4:00 Break
4:00-5:30 6 papers, dual track
Session 9A: Concurrency III (HBA, Chair: Rupak Majumdar, MPI-SWS)
A Calculus for Relaxed Memory
Karl Crary (Carnegie Mellon University)
Michael Sullivan (Carnegie Mellon University)
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
Ralf Jung (MPI-SWS, Germany)
David Swasey (MPI-SWS, Germany)
Filip Sieczkowski (Aarhus University)
Kasper Svendsen (Aarhus University)
Aaron Turon (Mozilla Research)
Lars Birkedal (Aarhus University)
Derek Dreyer (MPI-SWS, Germany)
Tractable Refinement Checking for Concurrent Objects
Ahmed Bouajjani (LIAFA Université Paris Diderot; France)
Michael Emmi (IMDEA Software Institute, Spain)
Constantin Enea (LIAFA Université Paris Diderot; France)
Jad Hamza (LIAFA Université Paris Diderot; France)
Session 9B: Synthesis (AG66, Chair: Swarat Chaudhuri, Rice University)
Decentralizing SDN Policies
Oded Padon (Tel Aviv University)
Neil Immerman (University of Massachusetts, Amherst)
Aleksandr Karbyshev (Tel Aviv University)
Ori Lahav (Tel Aviv University)
Mooly Sagiv (Tel Aviv University)
Sharon Shoham (The Academic College of Tel Aviv Yaffo)
Program Boosting: Program Synthesis via Crowd-Sourcing
Robert A Cochran (University of North Carolina at Chapel Hill)
Loris D'Antoni (University of Pennsylvania)
Benjamin Livshits (Microsoft Research)
David Molnar (Microsoft Research)
Margus Veanes (Microsoft Research)
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
Benjamin Delaware (MIT CSAIL)
Clément Pit-Claudel (MIT CSAIL)
Jason Gross (MIT CSAIL)
Adam Chlipala (MIT CSAIL)