PROGRAMMING LANGUAGES AND SYSTEMS (PB 2009)

Invited Talks.- The Twilight Zone: From Testing to Formal Specifications and Back Again.- Types and Recursion Schemes for Higher-Order Program Verification.- The Sketching Approach to Program Synthesis.- Program Analysis.- Large Spurious Cycle in Global Static Analyses and Its Algorithmic Mitigation.- Abstract Transformers for Thread Correlation Analysis.- Scalable Context-Sensitive Points-to Analysis Using Multi-dimensional Bloom Filters.- Transformation and Optimization.- A Short Cut to Optimal Sequences.- A Skeletal Parallel Framework with Fusion Optimizer for GPGPU Programming.- Witnessing Purity, Constancy and Mutability.- Type System.- On the Decidability of Subtyping with Bounded Existential Types.- Fractional Ownerships for Safe Memory Deallocation.- Ownership Downgrading for Ownership Types.- Separation Logic.- A Fresh Look at Separation Algebras and Share Accounting.- Weak updates and separation logic.- Proving Copyless Message Passing.- Logic and Foundation Theory.- On Stratified Regions.- Parallel Reduction in Resource Lambda-Calculus.- Classical Natural Deduction for S4 Modal Logic.- Software Security and Verification.- Bi-abductive Resource Invariant Synthesis.- Certify Once, Trust Anywhere: Modular Certification of Bytecode Programs for Certified Virtual Machine.- Asymptotic Resource Usage Bounds.- The Higher-Order, Call-by-Value Applied Pi-Calculus.- Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable.- Refining Abstract Interpretation-Based Static Analyses with Hints.