LEADER 04421nam 2200553 a 450 001 9910483929003321 005 20200520144314.0 010 $a3-540-71316-6 024 7 $a10.1007/978-3-540-71316-6 035 $a(CKB)1000000000490890 035 $a(SSID)ssj0000319598 035 $a(PQKBManifestationID)11240715 035 $a(PQKBTitleCode)TC0000319598 035 $a(PQKBWorkID)10338124 035 $a(PQKB)10194283 035 $a(DE-He213)978-3-540-71316-6 035 $a(MiAaPQ)EBC3068399 035 $a(PPN)123726956 035 $a(EXLCZ)991000000000490890 100 $a20070205d2007 uy 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aProgramming languages and systems $e16th European Symposium on Programming, ESOP 2007, held as part of the Joint European Conferences on Theory and Practics [i.e. Practice] of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007 : proceedings /$fRocco De Nicola (ed.) 205 $a1st ed. 2007. 210 $aBerlin ;$aNew York $cSpringer$d2007 215 $a1 online resource (XVIII, 542 p.) 225 1 $aLecture notes in computer science ;$v4421 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-71314-X 320 $aIncludes bibliographical references and index. 327 $aInvited Talk -- Techniques for Contextual Equivalence in Higher-Order, Typed Languages -- Models and Languages for Web Services -- Structured Communication-Centred Programming for Web Services -- CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements -- A Calculus for Orchestration of Web Services -- A Concurrent Calculus with Atomic Transactions -- Verification -- Modal I/O Automata for Interface and Product Line Theories -- Using History Invariants to Verify Observers -- Term Rewriting -- On the Implementation of Construction Functions for Non-free Concrete Data Types -- Anti-pattern Matching -- Language Based Security -- A Certified Lightweight Non-interference Java Bytecode Verifier -- Controlling the What and Where of Declassification in Language-Based Security -- Cost Analysis of Java Bytecode -- Logics and Correctness Proofs -- On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning -- Abstract Predicates and Mutable ADTs in Hoare Type Theory -- Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic -- Static Analysis and Abstract Interpretation I -- Modular Shape Analysis for Dynamically Encapsulated Programs -- Static Analysis by Policy Iteration on Relational Domains -- Computing Procedure Summaries for Interprocedural Analysis -- Small Witnesses for Abstract Interpretation-Based Proofs -- Static Analysis and Abstract Interpretation II -- Interprocedurally Analysing Linear Inequality Relations -- Precise Fixpoint Computation Through Strategy Iteration -- Semantic Theories for Object Oriented Languages -- A Complete Guide to the Future -- The Java Memory Model: Operationally, Denotationally, Axiomatically -- Immutable Objects for a Java-Like Language -- Process Algebraic Techniques -- Scalar Outcomes Suffice for Finitary Probabilistic Testing -- Probabilistic Anonymity Via Coalgebraic Simulations -- A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract) -- A Core Calculus for a Comparative Analysis of Bio-inspired Calculi -- Applicative Programming -- A Rewriting Semantics for Type Inference -- Principal Type Schemes for Modular Programs -- A Consistent Semantics of Self-adjusting Computation -- Multi-language Synchronization -- Types for Systems Properties -- Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts -- Type Reconstruction for General Refinement Types -- Dependent Types for Low-Level Programming. 410 0$aLecture notes in computer science ;$v4421. 606 $aComputer programming$vCongresses 606 $aProgramming languages (Electronic computers)$vCongresses 615 0$aComputer programming 615 0$aProgramming languages (Electronic computers) 676 $a005.1 701 $aDe Nicola$b Rocco$0104115 712 12$aETAPS 2007$f(2007 :$eBraga, Portugal) 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483929003321 996 $aProgramming languages and systems$94194633 997 $aUNINA