List of accepted
papers
- Multiple Facets for Dynamic Information
Flow. Authors:
Thomas Austin and Cormac Flanagan (UC Santa Cruz)
- A Unified Approach to Fully Lazy Sharing.
Authors:
Thibaut
Balabonski (PPS, Université Paris-Diderot)
- An Executable Formal
Semantics of C with Applications.
Authors:
Chucky Ellison and Grigore
Rosu (University of Illinois)
- Defining Code-injection
Attacks.
Authors:
Donald Ray and Jay Ligatti (University of South
Florida)
- The Marriage of Bisimulations and Kripke Logical
Relations.
Authors:
Chung-Kil Hur, Derek Dreyer, Georg Neis, and
Viktor Vafeiadis (MPI-SWS)
- Recursive Proofs for Inductive Tree
Data-Structures.
Authors:
P. Madhusudan, Xiaokang Qiu, and Andrei
Stefanescu (Univ of Illinois at Urbana-Champaign)
- An Abstract
Interpretation Framework for Termination. Authors:
Patrick Cousot
(CNRS ENS INRIA NYU) and Radhia Cousot (CNRS ENS INRIA)
-
Algebraic Foundations for Effect-Dependent Optimisations.
Authors:
Ohad Kammar and Gordon Plotkin (University of Edinburgh)
- Higher-Order Functional Reactive Programming in Bounded Space.
Authors:
Neelakantan R. Krishnaswami and Nick Benton (Microsoft Research)
and Jan Hoffmann (LMU Munich)
- Optimal Randomized Transformation
of Approximate Computations. Authors:
Zeyuan Allen Zhu, Sasa
Misailovic, Jonathan Kelner, and Martin Rinard (MIT)
- Clarifying
and compiling C/C++ concurrency: from C++0x to POWER.
Authors:
Mark
Batty (University of Cambridge), Kayvan Memarian (INRIA), and Scott Owens,
Susmit Sarkar, and Peter Sewell (University of Cambridge)
- A
Compiler and Run-time System for Network Programming Languages.
Authors:
Christopher Monsanto (Princeton University), Nate Foster
(Cornell University), Rob Harrison (United States Military Academy), and
David Walker (Princeton University)
- Information Effects.
Authors:
Roshan James and Amr Sabry (Indiana University)
- A
Language for Automatically Enforcing Privacy Policies. Authors:
Jean
Yang, Kuat Yessenov, and Armando Solar-Lezama (MIT CSAIL)
- Static
and User-Extensible Proof Checking. Authors:
Antonis Stampoulis and
Zhong Shao (Yale University)
- A Rely-Guarantee-Based Simulation
for Verifying Concurrent Program Transformations. Authors:
Hongjin
Liang, Xinyu Feng, and Ming Fu (School of Computer Science and Technology,
University of Science and Technology of China)
- A Type Theory for
Probability Density Functions. Authors: Sooraj Bhat (College of
Computing, Georgia Institute of Technology), Ashish Agarwal (Courant
Institute of Mathematical Sciences, New York University), and Richard
Vuduc and Alexander Gray (College of Computing, Georgia Institute of
Technology)
- Abstractions From Tests. Authors:
Mayur Naik
(Georgia Tech), Hongseok Yang (Oxford University), and Ghila Castelnuovo
and Mooly Sagiv (Tel-Aviv University)
- A mechanized semantics for
C++ object construction and destruction, with applications to resource
management.
Authors:
Tahina Ramananandro (INRIA Paris-Rocquencourt),
Gabriel Dos Reis (Texas A&M University), and Xavier Leroy (INRIA
Paris-Rocquencourt)
- Programming with Binders and Indexed
Data-Types.
Authors:
Andrew Cave and Brigitte Pientka (McGill
University)
- Analysis of Recursively Parallel Programs.
Authors:
Ahmed Bouajjani and Michael Emmi (LIAFA, Université Paris
Diderot, France)
- Access Permission Contracts for Scripting
Languages. Authors:
Phillip Heidegger, Annette Bieniusa, and Peter
Thiemann (University of Freiburg)
- Canonicity for 2-Dimensional
Type Theory.
Authors:
Daniel R. Licata and Robert Harper (Carnegie
Mellon University)
- Freefinement. Authors:
Stephan van Staden
(ETH Zurich), Cristiano Calcagno (ETH Zurich, Imperial College London and
Monoidics Ltd), and Bertrand Meyer (ETH Zurich)
- Towards Nominal
Computation.
Authors:
Mikolaj Bojanczyk, Laurent Braud, Bartek Klin,
and Slawomir Lasota (University of Warsaw)
- Resource-Sensitive
Synchronization Inference by Abduction. Authors:
Matko Botincan and
Mike Dodds (University of Cambridge) and Suresh Jagannathan (Purdue
University)
- Underspecified harnesses and interleaved bugs.
Authors:
Saurabh Joshi (IIT Kanpur), Shuvendu Lahiri (Microsoft Research,
Redmond), and Akash Lal (Microsoft Research, Bangalore)
-
Constraints as Control.
Authors:
Ali Sinan Köksal, Viktor Kuncak, and
Philippe Suter (EPFL)
- Edit Lenses. Authors:
Martin Hofmann
(Ludwig Maximilians Universität) and Benjamin C. Pierce and Daniel Wagner
(University of Pennsylvania)
- Sound Predictive Race Detection in
Polynomial Time.
Authors:
Yannis Smaragdakis (University of Athens and
UMass Amherst), Jacob M. Evans (University of Massachusetts at Amherst),
and Caitlin Sadowski, Jaeheon Yi, and Cormac Flanagan (University of
California at Santa Cruz)
- Symbolic Finite State Transducers,
Algorithms and Applications. Authors:
Nikolaj Bjorner (Microsoft
Research), Pieter Hooimeijer (U. Virginia), and Benjamin Livshits, David
Molnar, and Margus Veanes (Microsoft Research)
- Run Your Research:
On the Effectiveness of Lightweight Mechanization. Authors:
Casey
Klein (Northwestern University), John Clements (California Polytechnic
State University), Christos Dimoulas, Carl Eastlund, and Matthias
Felleisen (Northeastern University), Matthew Flatt (University of Utah),
Jay McCarthy (Brigham Young University), Jon Rafkind (University of Utah),
Sam Tobin-Hochstadt (Northeastern University), and Robert Bruce Findler
(Northwestern University)
- Extending System F-eta with Abstraction
over Erasable Coercions.
Authors:
Didier Remy and Julien Cretin
(INRIA Paris-Rocquencourt)
- A Program Logic for JavaScript.
Authors:
Philippa Gardner, Sergio Maffeis, and Gareth Smith (Imperial
College London)
- Deciding Choreography Realizability.
Authors:
Samik Basu (Iowa State University), Tevfik Bultan (University of
California at Santa Barbara), and Meriem Ouederni (University of
Malagna)
- Nested Refinements: A Logic for Duck Typing.
Authors:
Ravi Chugh, Patrick M. Rondon, and Ranjit Jhala
(UC San Diego)
- The Ins and Outs of Gradual Type
Inference.
Authors:
Aseem Rastogi (SUNY Stony Brook) and Avik
Chaudhuri and Basil Hosmer (Adobe Advanced Technology Labs)
- A
Type System for Borrowing Without Fractions.
Authors:
Karl Naden
(Carnegie Mellon University),
Robert L. Bocchino Jr. (Carnegie Mellon University), Kevin Bierhoff (Two
Sigma), and
Jonathan Aldrich (Carnegie Mellon
University)
-
Formalizing the LLVM Intermediate Representation for
Verified Program Transformation.
Authors:
Jianzhou Zhao, Steve
Zdancewic, Santosh Nagarakatte, and Milo M. K. Martin (University of
Pennsylvania)
- Self-Certification: Bootstrapping Certified
Typecheckers in F* with Coq.
Authors:
Pierre-Yves Strub (MSR INRIA)
and Nikhil Swamy, Cedric Fournet, and Juan Chen (Microsoft
Research)
- Verification of Parameterized Concurrent Programs
By Modular Reasoning about Data and Control. Authors:
Azadeh Farzan
and Zachary Kincaid (University of Toronto)
- Probabilistic
Relational Reasoning for Differential Privacy.
Authors:
Gilles
Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Beguelin (IMDEA
Software Institute)
- Playing in the Grey Area of Proofs.
Authors:
Krystof Hoder (University of Manchester), Laura Kovacs (TU
Vienna), and Andrei Voronkov (University of Manchester)
- Syntactic
Control of Interference for Separation Logic.
Authors:
Uday S. Reddy
(University of Birmingham) and John C. Reynolds
(Carnegie-Mellon)