Abstract is missing.
- The Audacity of Hope: Thoughts on Reclaiming the Database DreamSam Lindley, Philip Wadler. 1 [doi]
- Dynamic Boundaries: Information Hiding by Second Order Framing with First Order AssertionsDavid A. Naumann, Anindya Banerjee. 2-22 [doi]
- Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static AnalysisAssalé Adjé, Stephane Gaubert, Eric Goubault. 23-42 [doi]
- Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with ArraysTorben Amtoft, John Hatcliff, Edwin RodrÃguez. 43-63 [doi]
- A Semantic Framework for Declassification and EndorsementAslan Askarov, Andrew Myers. 64-84 [doi]
- Amortised Resource Analysis with Separation LogicRobert Atkey. 85-103 [doi]
- A PolyTime Functional Language from Light Linear LogicPatrick Baillot, Marco Gaboardi, Virgile Mogbil. 104-124 [doi]
- Testing Polymorphic PropertiesJean-Philippe Bernardy, Patrik Jansson, Koen Claessen. 125-144 [doi]
- Formal Verification of Coalescing Graph-Coloring Register AllocationSandrine Blazy, Benoît Robillard, Andrew W. Appel. 145-164 [doi]
- A Theory of Speculative ComputationGérard Boudol, Gustavo Petri. 165-184 [doi]
- Propositional Interpolation and Abstract InterpretationVijay D Silva. 185-204 [doi]
- Functional Programming in Sublinear SpaceUgo Dal Lago, Ulrich Schöpp. 205-225 [doi]
- Logical Concurrency Control from Sequential ProofsJyotirmoy Deshmukh, Ganesan Ramalingam, Venkatesh Prasad Ranganath, Kapil Vaswani. 226-245 [doi]
- Fluid Updates: Beyond Strong vs. Weak UpdatesIsil Dillig, Thomas Dillig, Alex Aiken. 246-266 [doi]
- Parameterized Memory Models and Concurrent Separation LogicRodrigo Ferreira, Xinyu Feng, Zhong Shao. 267-286 [doi]
- Amortized Resource Analysis with Polynomial PotentialJan Hoffmann 0002, Martin Hofmann. 287-306 [doi]
- Generative Operational Semantics for Relaxed Memory ModelsRadha Jagadeesan, Corin Pitcher, James Riely. 307-326 [doi]
- Automating Security Mediation PlacementDave King 0002, Susmit Jha, Divya Muthukumaran, Trent Jaeger, Somesh Jha, Sanjit A. Seshia. 327-344 [doi]
- TRX: A Formally Verified Parser InterpreterAdam Koprowski, Henri Binsztok. 345-365 [doi]
- On the Expressive Power of Primitives for Compensation HandlingIvan Lanese, Cátia Vaz, Carla Ferreira. 366-386 [doi]
- Separating Shape GraphsVincent Laviron, Bor-Yuh Evan Chang, Xavier Rival. 387-406 [doi]
- Deadlock-Free Channels and LocksK. Rustan M. Leino, Peter Müller, Jan Smans. 407-426 [doi]
- Verifying a Compiler for Java ThreadsAndreas Lochbihler. 427-447 [doi]
- A Grammar-Based Approach to Invertible ProgramsKazutaka Matsuda, Shin-Cheng Mu, Zhenjiang Hu, Masato Takeichi. 448-467 [doi]
- Faulty Logic: Reasoning about Fault Tolerant ProgramsMatthew L. Meola, David Walker. 468-487 [doi]
- A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of WhileKeiko Nakata, Tarmo Uustalu. 488-506 [doi]
- A Universal Calculus for Stream Processing LanguagesRobert Soulé, Martin Hirzel, Robert Grimm, Bugra Gedik, Henrique Andrade, Vibhore Kumar, Kun-Lung Wu. 507-528 [doi]
- Enforcing Stateful Authorization and Information Flow Policies in FineNikhil Swamy, Juan Chen, Ravi Chugh. 529-549 [doi]
- Stateful Contracts for Affine TypesJesse A. Tov, Riccardo Pucella. 550-569 [doi]
- CFA2: A Context-Free Approach to Control-Flow AnalysisDimitrios Vardoulakis, Olin Shivers. 570-589 [doi]
- Weighted Dynamic Pushdown NetworksAlexander Wenner. 590-609 [doi]
- Explicit Stabilisation for Modular Rely-Guarantee ReasoningJohn Wickerson, Mike Dodds, Matthew J. Parkinson. 610-629 [doi]