Programming Languages and Systems: 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings

Front Matter....Pages -
The Twilight Zone: From Testing to Formal Specifications and Back Again....Pages 1-1
Types and Recursion Schemes for Higher-Order Program Verification....Pages 2-3
The Sketching Approach to Program Synthesis....Pages 4-13
Large Spurious Cycle in Global Static Analyses and Its Algorithmic Mitigation....Pages 14-29
Abstract Transformers for Thread Correlation Analysis....Pages 30-46
Scalable Context-Sensitive Points-to Analysis Using Multi-dimensional Bloom Filters....Pages 47-62
A Short Cut to Optimal Sequences....Pages 63-78
A Skeletal Parallel Framework with Fusion Optimizer for GPGPU Programming....Pages 79-94
Witnessing Purity, Constancy and Mutability....Pages 95-110
On the Decidability of Subtyping with Bounded Existential Types....Pages 111-127
Fractional Ownerships for Safe Memory Deallocation....Pages 128-143
Ownership Downgrading for Ownership Types....Pages 144-160
A Fresh Look at Separation Algebras and Share Accounting....Pages 161-177
Weak updates and separation logic....Pages 178-193
Proving Copyless Message Passing....Pages 194-209
On Stratified Regions....Pages 210-225
Parallel Reduction in Resource Lambda-Calculus....Pages 226-242
Classical Natural Deduction for S4 Modal Logic....Pages 243-258
Bi-abductive Resource Invariant Synthesis....Pages 259-274
Certify Once, Trust Anywhere: Modular Certification of Bytecode Programs for Certified Virtual Machine....Pages 275-293
Asymptotic Resource Usage Bounds....Pages 294-310
The Higher-Order, Call-by-Value Applied Pi-Calculus....Pages 311-326
Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable....Pages 327-342
Refining Abstract Interpretation-Based Static Analyses with Hints....Pages 343-358
Back Matter....Pages -