LEADER 04709nam 22007935 450 001 9910483343303321 005 20251226200514.0 010 $a3-642-10672-2 024 7 $a10.1007/978-3-642-10672-9 035 $a(CKB)1000000000812693 035 $a(SSID)ssj0000355591 035 $a(PQKBManifestationID)11227498 035 $a(PQKBTitleCode)TC0000355591 035 $a(PQKBWorkID)10340648 035 $a(PQKB)10485189 035 $a(DE-He213)978-3-642-10672-9 035 $a(MiAaPQ)EBC3064886 035 $a(PPN)139962972 035 $a(EXLCZ)991000000000812693 100 $a20100301d2009 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aProgramming Languages and Systems $e7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009, Proceedings /$fedited by Zhenjiang Hu 205 $a1st ed. 2009. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2009. 215 $a1 online resource (X, 359 p.) 225 1 $aProgramming and Software Engineering,$x2945-9168 ;$v5904 300 $aInternational conference proceedings. 311 08$a3-642-10671-4 320 $aIncludes bibliographical references and index. 327 $aInvited 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. 330 $aThis book constitutes the refereed proceedings of the 7th Asian Symposium on Programming Languages and Systems, APLAS 2009, held in Seoul, Korea, in December 2009. The 21 papers presented in this volume together with 3 invited talks were carefully reviewed and selected from 56 submissions. The papers are divided into topical sections on program analysis, transformation and optimization, type system, separation logic, logic and foundation theory, software security and verification, and software security and verification. 410 0$aProgramming and Software Engineering,$x2945-9168 ;$v5904 606 $aCompilers (Computer programs) 606 $aSoftware engineering 606 $aData protection 606 $aComputer science 606 $aComputer programming 606 $aCompilers and Interpreters 606 $aSoftware Engineering 606 $aData and Information Security 606 $aComputer Science Logic and Foundations of Programming 606 $aProgramming Techniques 615 0$aCompilers (Computer programs) 615 0$aSoftware engineering. 615 0$aData protection. 615 0$aComputer science. 615 0$aComputer programming. 615 14$aCompilers and Interpreters. 615 24$aSoftware Engineering. 615 24$aData and Information Security. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aProgramming Techniques. 676 $a005.13 686 $aDAT 310f$2stub 686 $aDAT 350f$2stub 686 $aSS 4800$2rvk 701 $aHu$b Zhenjiang$f1966-$01757732 712 12$aAPLAS 2009 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483343303321 996 $aProgramming languages and systems$94195679 997 $aUNINA