Table of Contents

• Engineering mathematics: the odd order theorem proofGeorges Gonthier. 1-2 [doi]
• Full abstraction for nominal Scott domainsSteffen Lösch, Andrew M. Pitts. 3-14 [doi]
• The sequential semantics of producer effect systemsRoss Tate. 15-26 [doi]
• Copatterns: programming infinite structures by observationsAndreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer. 27-38 [doi]
• Cache and I/O efficent functional algorithmsGuy E. Blelloch, Robert Harper. 39-50 [doi]
• On the linear ranking problem for integer linear-constraint loopsAmir M. Ben-Amram, Samir Genaim. 51-62 [doi]
• Advanced automata minimizationRichard Mayr, Lorenzo Clemente. 63-74 [doi]
• Automating relatively complete verification of higher-order functional programsHiroshi Unno, Tachio Terauchi, Naoki Kobayashi 0001. 75-86 [doi]
• Abstraction and invariance for algebraically indexed typesRobert Atkey, Patricia Johann, Andrew Kennedy. 87-100 [doi]
• Static and dynamic semantics of NoSQL languagesVéronique Benzaken, Giuseppe Castagna, Kim Nguyen 0001, Jérôme Siméon. 101-114 [doi]
• Quantitative abstraction refinementPavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna. 115-128 [doi]
• Inductive data flow graphsAzadeh Farzan, Zachary Kincaid, Andreas Podelski. 129-142 [doi]
• Abstract conflict driven learningVijay D'Silva, Leopold Haller, Daniel Kroening. 143-154 [doi]
• The Lambda Lambda-Bar calculus: a dual calculus for unconstrained strategiesAlexis Goyet. 155-166 [doi]
• The geometry of typesUgo Dal Lago, Barbara Petit. 167-178 [doi]
• Universal properties of impure programming languagesSam Staton, Paul Blain Levy. 179-192 [doi]
• The power of parameterization in coinductive proofChung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis. 193-206 [doi]
• Meta-theory à la carteBenjamin Delaware, Bruno C. D. S. Oliveira, Tom Schrijvers. 207-218 [doi]
• A theorem prover for Boolean BIJonghyun Park, Jeongbong Seo, Sungwoo Park. 219-232 [doi]
• From principles to programming languages (and back)Shriram Krishnamurthi. 233-234 [doi]
• Library abstraction for C/C++ concurrencyMark Batty, Mike Dodds, Alexey Gotsman. 235-248 [doi]
• Fault tolerance via idempotenceGanesan Ramalingam, Kapil Vaswani. 249-262 [doi]
• Deadlock-freedom-by-design: multiparty asynchronous global programmingMarco Carbone, Fabrizio Montesi. 263-274 [doi]
• The type discipline of behavioral separationLuís Caires, João Costa Seco. 275-286 [doi]
• Views: compositional reasoning for concurrent programsThomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang. 287-300 [doi]
• High-level separation logic for low-level codeJonas Braband Jensen, Nick Benton, Andrew Kennedy. 301-314 [doi]
• How languages can save distributed computingAndrew C. Myers. 315-316 [doi]
• Quantitative relaxation of concurrent data structuresThomas A. Henzinger, Christoph M. Kirsch, Hannes Payer, Ali Sezgin, Ana Sokolova. 317-328 [doi]
• Plan B: a buffered memory model for JavaDelphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, Jan Vitek. 329-342 [doi]
• Logical relations for fine-grained concurrencyAaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer. 343-356 [doi]
• Linear dependent types for differential privacyMarco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, Benjamin C. Pierce. 357-370 [doi]
• Fully abstract compilation to JavaScriptCédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, Benjamin Livshits. 371-384 [doi]
• Towards fully automatic placement of security sanitizers and declassifiersBenjamin Livshits, Stephen Chong. 385-398 [doi]
• The principles and practice of probabilistic programmingNoah D. Goodman. 399-402 [doi]
• A model-learner pattern for bayesian reasoningAndrew D. Gordon, Mihhail Aizatulin, Johannes Borgström, Guillaume Claret, Thore Graepel, Aditya V. Nori, Sriram K. Rajamani, Claudio V. Russo. 403-416 [doi]
• Hyperstream processing systems: nonstandard modeling of continuous-time signalsKohei Suenaga, Hiroyoshi Sekine, Ichiro Hasuo. 417-430 [doi]
• HALO: haskell to logic through denotational semanticsDimitrios Vytiniotis, Simon L. Peyton Jones, Koen Claessen, Dan Rosén. 431-442 [doi]
• Sigma*: symbolic learning of input-output specificationsMatko Botincan, Domagoj Babic. 443-456 [doi]
• Checking NFA equivalence with bisimulations up to congruenceFilippo Bonchi, Damien Pous. 457-468 [doi]
• Synthesis of biological models from mutation experimentsAli Sinan Köksal, Yewen Pu, Saurabh Srivastava, Rastislav Bodík, Jasmin Fisher, Nir Piterman. 469-482 [doi]
• Sub-polyhedral scheduling using (unit-)two-variable-per-inequality polyhedraRamakrishna Upadrasta, Albert Cohen. 483-496 [doi]
• Optimizing data structures in high-level programs: new directions for extensible compilers based on stagingTiark Rompf, Arvind K. Sujeeth, Nada Amin, Kevin J. Brown, Vojin Jovanovic, HyoukJoong Lee, Manohar Jonnalagedda, Kunle Olukotun, Martin Odersky. 497-510 [doi]
• Principled parsing for indentation-sensitive languages: revisiting Landin's offside ruleMichael D. Adams. 511-522 [doi]
• The ramifications of sharing in data structuresAquinas Hobor, Jules Villard. 523-536 [doi]
• Complete instantiation-based interpolationNishant Totla, Thomas Wies. 537-548 [doi]
• Automatic detection of floating-point exceptionsEarl T. Barr, Thanh Vo, Vu Le, Zhendong Su. 549-560 [doi]
• Subjective auxiliary state for coarse-grained concurrencyRuy Ley-Wild, Aleksandar Nanevski. 561-574 [doi]