| Foundations of C++ / Bjarne Stroustrup |
| What's Decidable about Weak Memory Models? / Mohamed Faouzi Atig ; Ahmed Bouajjani ; Sebastian Burckhardt ; Madanlal Musuvathi |
| A Formally Verified SSA-Based Middle-End: Static Single Assignment Meets CompCert / Gilles Barthe ; Delphine Demange ; David Pichardie |
| Eventually Consistent Transactions / Daan Leijen ; Manuel Fähndrich ; Mooly Sagiv |
| Concurrent Library Correctness on the TSO Memory Model / Alexey Gotsman ; Hongseok Yang |
| Automated Verification of Equivalence Properties of Cryptographic Protocols / Rohit Chadha ; Stefan Ciobaca ; Steve Kremer |
| The Call-by-Need Lambda Calculus, Revisited / Stephen Chang ; Matthias Felleisen |
| A Compositional Specification Theory for Component Behaviours / Taolue Chen ; Chris Chilton ; Bengt Jonsson ; Marta Kwiatkowska |
| Probabilistic Abstract Interpretation / Patrick Cousot ; Michael Monerau |
| Multiparty Session Types Meet Communicating Automata / Pierre-Malo Deniélou ; Nobuko Yoshida |
| Complete Monitors for Behavioral Contracts / Christos Dimoulas ; Sam Tobin-Hochstadt |
| A Systematic Approach to Delimited Control with Multiple Prompts / Paul Downen ; Zena M. Ariola |
| Generate, Test, and Aggregate: A Calculation-Based Framework for Systematic Parallel Programming with MapReduce / Kento Emoto ; Sebastian Fischer ; Zhenjiang Hu |
| Trace Spaces: An Efficient New Technique for State-Space Reduction / Lisbeth Fajstrup ; Éric Goubault ; Emmanuel Haucourt ; Samuel Mimram ; Martin Raussen |
| A Process Algebra for Wireless Mesh Networks / Ansgar Fehnker ; Rob van Glabbeek ; Peter Höfner ; Annabelle McIver ; Marius Portmann ; Wee Lum Tan |
| On the Correctness of the SIMT Execution Model of GPUs / Axel Habermaier ; Alexander Knapp |
| Reasoning about Lock Placements / Peter Hawkins ; Alex Aiken ; Kathleen Fisher ; Martin Rinard |
| Reasoning about Multi-stage Programs / Jun Inoue ; Walid Taha |
| Fictional Separation Logic / Jonas Braband Jensen ; Lars Birkedal |
| Validating LR(1) Parsers / Jacques-Henri Jourdan ; François Pottier ; Xavier Leroy |
| Adding Equations to System F Types / Neelakantan R. Krishnaswami ; Nick Benton |
| GMeta: A Generic Formal Metatheory Framework for First-Order Representations / Gyesik Lee ; Bruno C.d.S. Oliveira ; Sungkeun Cho ; Kwangkeun Yi |
| Expansion for Universal Quantifiers / Sergueï Lenglet ; Joe B. Wells |
| Non-monotonic Self-Adjusting Computation / Ruy Ley-Wild ; Umut A. Acar ; Guy Blelloch |
| Java and the Java Memory Model - A Unified, Machine-Checked Formalisation / Andreas Lochbihler |
| A Type and Effect System for Determinism in Multithreaded Programs / Yi Lu ; John Potter ; Chenyi Zhang ; Jingling Xue |
| Linear Logical Relations for Session-Based Concurrency / Jorge A. Pérez ; Luís Caires ; Frank Pfenning ; Bernardo Toninho |
| Staged Computation with Staged Lexical Scope / Morten Rhiger |
| Gradual Ownership Types / Ilya Sergey ; Dave Clarke |
| Author Index |
| Foundations of C++ / Bjarne Stroustrup |
| What's Decidable about Weak Memory Models? / Mohamed Faouzi Atig ; Ahmed Bouajjani ; Sebastian Burckhardt ; Madanlal Musuvathi |
| A Formally Verified SSA-Based Middle-End: Static Single Assignment Meets CompCert / Gilles Barthe ; Delphine Demange ; David Pichardie |
| Eventually Consistent Transactions / Daan Leijen ; Manuel Fähndrich ; Mooly Sagiv |
| Concurrent Library Correctness on the TSO Memory Model / Alexey Gotsman ; Hongseok Yang |
| Automated Verification of Equivalence Properties of Cryptographic Protocols / Rohit Chadha ; Stefan Ciobaca ; Steve Kremer |
