Preliminary Session Schedule

Day/Time	Title	Papers
Session 0: Tue 19 Mar 2013 14:00-14:03; 14:03-15:30 Philippa Gardner; Matthias Felleisen	Programming Techniques	Mihai Budiu, Joel Galenson, Gordon D. Plotkin The Compiler Forest Microsoft Research Silicon Valley; University of California at Berkeley; University of Edinburgh Arthur Charguéraud Pretty-Big-Step Semantics INRIA Saclay; Université Paris Sud; CNRS Jean-Baptiste Jeannin, Dexter Kozen, Alexandra Silva Language Constructs for Non-Well-Founded Computation Cornell University; Radboud University Nijmegen
Session 1: Tue 19 Mar 2013 16:00-17:30 Matthias Felleisen	Programming Tools	Stephen Chang Laziness by Need Northeastern University Kazutaka Matsuda, Meng Wang FliPpr: A Prettier Invertible Printing System The University of Tokyo; Chalmers University of Technology María Alpuente, Demis Ballis, Francisco Frechina, Julia Sapiña Slicing-based Trace Analysis of Rewriting Logic Specifications with iJulienne Universitat Politècnica de València; Università degli Studi di Udine Jean-Christophe Filliâtre, Andrei Paskevich Why3---Where Programs Meet Provers Université Paris Sud; CNRS; INRIA Saclay
Session 2: Wed 20 Mar 2013 10:30-12:30 Philippa Gardener	Separation Logic	Constantin Enea, Vlad Saveluc, Mihaela Sighireanu Compositional Invariant Checking for Overlaid and Nested Linked Lists Université Paris Diderot; Sorbonne Paris Cite Ioannis T. Kassios, Eleftherios Kritikos A Discipline for Program Verification based on Backpointers and its Use in Observational Disjointness ETH Zurich; National Technical University of Athens Kasper Svendsen, Lars Birkedal, Matthew Parkinson Modular Reasoning about Separation of Concurrent Data Structures IT University of Copenhagen; Microsoft Research Cambridge John Wickerson, Mike Dodds, Matthew Parkinson Ribbon Proofs for Separation Logic Technische Universität Berlin; University of York; Microsoft Research Cambridge
Session 3: Wed 20 Mar 2013 14:00-15:00 Holger Hermanns	Gradual Typing	Niki Vazou, Patrick M. Rondon, Ranjit Jhala Abstract Refinement Types UC San Diego; Google Asumu Takikawa, T. Stephen Strickland, Sam Tobin-Hochstadt Constraining Delimited Control with Contracts Northeastern University; University of Maryland at College Park
Session 4: Wed 20 Mar 2013 16:30-18:00 Martin Hofmann	Shared-memory Concurrency and Verification	Alexey Gotsman, Noam Rinetzky, Hongseok Yang Verifying Concurrent Memory Reclamation Algorithms with Grace IMDEA Software Institute; Tel-Aviv University; University of Oxford Peter Collingbourne, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels Imperial College London; Microsoft Research Cambridge Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza Verifying Concurrent Programs against Sequential Specifications Université Paris Diderot
Session 5: Thu 21 Mar 2013 10:30-12:30 Yannis Smaragdakis	Process Calculi	Kirstin Peters, Uwe Nestmann, Ursula Goltz On Distributability in Process Calculi TU Berlin; TU Braunschweig Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho Behavioral Polymorphism and Parametricity in Session-Based Communication Universidade Nova de Lisboa; Carnegie Mellon University Bernardo Toninho, Luís Caires, Frank Pfenning Higher-Order Processes, Functions, and Sessions: A Monadic Integration Carnegie Mellon University; Universidade Nova de Lisboa Ivan Lanese, Michael Lienhardt, Claudio Antares Mezzina, Alan Schmitt, Jean-Bernard Stefani Concurrent Flexible Reversibility University of Bologna; Paris Diderot University; FBK, Trento; INRIA
Session 6: Thu 21 Mar 2013 15:15-16:15 Didier Remy	Taming Concurrency	Yi Lu, John Potter, Jingling Xue Structural Lock Correlation with Ownership Types University of New South Wales at Sydney Joost-Peter Katoen, Doron Peled Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems RWTH Aachen University; University of Twente; Bar Ilan University Ramat Gan
Session 7: Thu 21 Mar 2013 16:30-18:00 Ranjit Jhala	Model Checking and Verification	Naoki Kobayashi, Atsushi Igarashi Model-Checking Higher-Order Programs with Recursive Types The University of Tokyo; Kyoto Univeristy Mohamed Nassim Seghir, Daniel Kroening Counterexample-guided Precondition Inference University of Oxford Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith Information Reuse for Multi-goal Reachability Analyses University of Passau; Vienna University of Technology; University of Oxford; Queen Mary University of London
Session 8: Fri 22 Mar 2013 11:00-12:30 Scott Owens	Weak-memory Concurrency and Verification	Radha Jagadeesan, Gustavo Petri, Corin Pitcher, James Riely Quarantining Weakness DePaul University; Purdue University Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig Software Verification for Weak Memory via Program Transformation University College London; University of Oxford; Queen Mary University of London Ahmed Bouajjani, Egor Derevenetc, Roland Meyer Checking and Enforcing Robustness against TSO University Paris 7; Fraunhofer ITWM; University of Kaiserslautern
Session 9: Fri 22 Mar 2013 14:00-15:00 Philippa Gardner	Special ETAPS Session: Invited Talk	Mark S. Miller, Tom Van Cutsem, Bill Tulloh Distributed Electronic Rights in JavaScript Google; Vrije Universiteit Brussel
Session 10: Fri 22 Mar 2013 16:30-18:00 Annie Liu	Types, Inference, and Analysis	Gabriel Scherer, Didier Rémy GADTs meet subtyping INRIA Rocquencourt Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, Aditya V. Nori A Data Driven Approach for Algebraic Loop Invariants Stanford University; University of California at Berkeley; Microsoft Research India Martin Hofmann, Dulma Rodriguez Automatic Type Inference for Amortised Heap-Space Analysis University of Munich; Monoidics Ltd