ESOP 2012 - Preliminary Programme
Monday, March 26,2012
Theory of Functional Programming (11:00-12:30)
Stephen Chang and Matthias Felleisen.
The Call-by-need Lambda Calculus, Revisited
Christos Dimoulas, Sam Tobin-Hochstadt and Matthias Felleisen.
Complete Monitoring for Behavioral Contracts
Paul Downen and Zena M. Ariola.
A Systematic Approach to Delimited Control with Multiple Prompts
Type Systems (14:00-15:30)
Ilya Sergey and Dave Clarke.
Gradual Ownership Types
Neelakantan Krishnaswami and Nick Benton.
Adding Equations to System F
Sergueï Lenglet and Joe Wells.
Expansion for Universal Quantifiers
Analysis (14:00-15:30)
Patrick Cousot and Michael Monerau.
Probabilistic Abstract Interpretation
Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram and Martin Raussen.
Trace Spaces: an Efficient New Technique for State-Space Reduction
Taolue Chen, Chris Chilton, Bengt Jonsson and Marta Kwiatkowska.
A Compositional Specification Theory for Component Behaviours
Jonas Braband Jensen and Lars Birkedal.
Fictional Separation Logic
Tuesday, March 27,2012
Parallelism (10:30-12:30)
Kento Emoto, Sebastian Fischer and Zhenjiang Hu.
Generate, Test, and Aggregate ---A Calculation-based Framework for Systematic Parallel Programming with MapReduce
Axel Habermaier and Alexander Knapp.
On the Correctness of the SIMT Execution Model of GPUs
Yi Lu, John Potter, Chenyi Zhang and Jingling Xue.
A Type and Effect System for Determinism in Multithreaded Programs
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard and Mooly Sagiv.
Reasoning About Lock Placements
Staged Computation (15:10-16:10)
Morten Rhiger.
Staged Computation with Staged Lexical Scope
Jun Inoue and Walid Taha.
Reasoning About Multi-Stage Programs
Processes and Sessions (16:30-18:00)
Ansgar Fehnker, Rob Van Glabbeek, Peter Höfner, Annabelle Mciver, Marius Portmann and Wee Lum Tan.
A Process Algebra for Wireless Mesh Networks
Pierre-Malo Denielou and Nobuko Yoshida.
Multiparty Session Types Meet Communicating Automata
Jorge A. Pérez, Luis Caires, Frank Pfenning and Bernardo Toninho.
Linear Logical Relations for Session-Based Concurrency
Wednesday, March 28,2012
Verification (10:30-12:30)
Andreas Lochbihler.
Java and the Java Memory Model - a Unified, Machine-Checked Formalisation
Gilles Barthe, Delphine Demange and David Pichardie.
A formally verified SSA-based middle-end -- Single Static Assignment meets CompCert
Rohit Chadha, Stefan Ciobaca and Steve Kremer.
Automated verification of equivalence properties of cryptographic protocols
Jacques-Henri Jourdan, François Pottier and Xavier Leroy.
Validating LR(1) Parsers
Weak Memory Models (15:10-16:10)
Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi and Hongseok Yang.
Concurrent library correctness on the TSO memory model
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt and Madanlal Musuvathi.
What's Decidable About Weak Memory Models?
Models of Programming (16:30-18:00)
Gyesik Lee, Bruno C. D. S. Oliveira, Sungkeun Cho and Kwangkeun Yi.
GMeta: A Generic Formal Metatheory Framework for First-Order Representations
Ruy Ley-Wild, Umut Acar and Guy Blelloch.
Non-Monotonic Self-Adjusting Computation
Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen and Mooly Sagiv.
Eventually Consistent Transactions