Table of Contents

• Automating Repetitive Tasks for the MassesSumit Gulwani. 1-2 [doi]
• Functors are Type Refinement SystemsPaul-André Melliès, Noam Zeilberger. 3-16 [doi]
• Integrating Linear and Dependent TypesNeelakantan R. Krishnaswami, Pierre Pradic, Nick Benton. 17-30 [doi]
• Higher Inductive Types as Homotopy-Initial AlgebrasKristina Sojakova. 31-42 [doi]
• Runtime Enforcement of Security Policies on Black Box Reactive ProgramsMinh Ngo, Fabio Massacci, Dimiter Milushev, Frank Piessens. 43-54 [doi]
• Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential PrivacyGilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub. 55-68 [doi]
• Differential Privacy: Now it's Getting PersonalHamid Ebadi, David Sands, Gerardo Schneider. 69-81 [doi]
• Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of CallbacksHao Tang, Xiaoyin Wang, Lingming Zhang, Bing Xie, Lu Zhang 0023, Hong Mei. 83-95 [doi]
• Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant TreewidthKrishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, Prateesh Goyal. 97-109 [doi]
• Predicting Program Properties from "Big Code"Veselin Raychev, Martin T. Vechev, Andreas Krause. 111-124 [doi]
• DReX: A Declarative Language for Efficiently Evaluating Regular String TransformationsRajeev Alur, Loris D'Antoni, Mukund Raghothaman. 125-137 [doi]
• Data-Parallel String-Manipulating ProgramsMargus Veanes, Todd Mytkowicz, David Molnar, Benjamin Livshits. 139-152 [doi]
• Ur/Web: A Simple Model for Programming the WebAdam Chlipala. 153-165 [doi]
• Safe & Efficient Gradual Typing for TypeScriptAseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin M. Bierman, Panagiotis Vekris. 167-180 [doi]
• Space-Efficient Manifest ContractsMichael Greenberg. 181-194 [doi]
• Manifest Contracts for DatatypesTaro Sekiyama, Yuki Nishida, Atsushi Igarashi. 195-207 [doi]
• Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about itViktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli. 209-220 [doi]
• From Communicating Machines to Graphical ChoreographiesJulien Lange, Emilio Tuosto, Nobuko Yoshida. 221-232 [doi]
• A Scalable, Correct Time-Stamped StackMike Dodds, Andreas Haas, Christoph M. Kirsch. 233-246 [doi]
• A Formally-Verified C Static AnalyzerJacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie. 247-259 [doi]
• Analyzing Program AnalysesRoberto Giacobazzi, Francesco Logozzo, Francesco Ranzato. 261-273 [doi]
• Compositional CompCertGordon Stewart, Lennart Beringer, Santiago Cuellar, Andrew W. Appel. 275-287 [doi]
• Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type ReconstructionGiuseppe Castagna, Kim Nguyen 0001, Zhiwu Xu, Pietro Abate. 289-302 [doi]
• Principal Type Schemes for Gradual ProgramsRonald Garcia, Matteo Cimini. 303-315 [doi]
• Dependent Information Flow TypesLuísa Lourenço, Luís Caires. 317-328 [doi]
• Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executablesMila Dalla Preda, Roberto Giacobazzi, Arun Lakhotia, Isabella Mastroeni. 329-341 [doi]
• A Coalgebraic Decision Procedure for NetKATNate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva 0001, Laure Thompson. 343-355 [doi]
• Symbolic Algorithms for Language Equivalence and Kleene Algebra with TestsDamien Pous. 357-368 [doi]
• Programming up to CongruenceVilhelm Sjöberg, Stephanie Weirich. 369-382 [doi]
• A Meta Lambda Calculus with Cross-Level ComputationKazunori Tobisawa. 383-393 [doi]
• Algebraic Effects, Linearity, and Quantum Programming LanguagesSam Staton. 395-406 [doi]
• Proof Spaces for Unbounded ParallelismAzadeh Farzan, Zachary Kincaid, Andreas Podelski. 407-420 [doi]
• Equations, Contractions, and Unique SolutionsDavide Sangiorgi. 421-432 [doi]
• Succinct Representation of Concurrent Trace SetsAshutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta, Thorsten Tarrach. 433-444 [doi]
• K-Java: A Complete Semantics of JavaDenis Bogdanas, Grigore Rosu. 445-456 [doi]
• Towards the Essence of HygieneMichael D. Adams. 457-469 [doi]
• Self-Representation in Girard's System UMatt Brown, Jens Palsberg. 471-484 [doi]
• Coding by Everyone, Every DayPeter Lee. 485 [doi]
• Databases and Programming: Two Subjects Divided by a Common Language?Peter Buneman. 487 [doi]
• Probabilistic Termination: Soundness, Completeness, and CompositionalityLuis María Ferrer Fioriti, Holger Hermanns. 489-501 [doi]
• Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic SystemsFei He, Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang. 503-514 [doi]
• Full Abstraction for Signal Flow GraphsFilippo Bonchi, Pawel Sobocinski, Fabio Zanasi. 515-526 [doi]
• Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion SchemesRalf Hinze, Nicolas Wu, Jeremy Gibbons. 527-538 [doi]
• Quantitative Interprocedural AnalysisKrishnendu Chatterjee, Andreas Pavlogiannis, Yaron Velner. 539-551 [doi]
• Specification Inference Using Context-Free Language ReachabilityOsbert Bastani, Saswat Anand, Alex Aiken. 553-566 [doi]
• On Characterizing the Data Access Complexity of ProgramsVenmugil Elango, Fabrice Rastello, Louis-Noël Pouchet, J. Ramanujam, P. Sadayappan. 567-580 [doi]
• Sound Modular Verification of C Code Executing in an Unverified ContextPieter Agten, Bart Jacobs 0002, Frank Piessens. 581-594 [doi]
• Deep Specifications and Certified Abstraction LayersRonghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, Yu Guo. 595-608 [doi]
• From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program VerificationAdam Chlipala. 609-622 [doi]
• A Calculus for Relaxed MemoryKarl Crary, Michael J. Sullivan. 623-636 [doi]
• Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent ReasoningRalf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer. 637-650 [doi]
• Tractable Refinement Checking for Concurrent ObjectsAhmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza. 651-662 [doi]
• Decentralizing SDN PoliciesOded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham. 663-676 [doi]
• Program Boosting: Program Synthesis via Crowd-SourcingRobert A. Cochran, Loris D'Antoni, Benjamin Livshits, David Molnar, Margus Veanes. 677-688 [doi]
• Fiat: Deductive Synthesis of Abstract Data Types in a Proof AssistantBenjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala. 689-700 [doi]