Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Programming Languages and Systems [[electronic resource] ] : 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings / / edited by Hongseok Yang
| Programming Languages and Systems [[electronic resource] ] : 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings / / edited by Hongseok Yang |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XV, 992 p. 236 illus.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Compilers (Computer programs)
Computer science Software engineering Computer programming Compilers and Interpreters Computer Science Logic and Foundations of Programming Software Engineering Theory of Computation Programming Techniques |
| ISBN | 3-662-54434-2 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Disjoint Polymorphism -- Generalizing inference systems by coaxioms -- Observed Communication Semantics for Classical Processes -- Is your software on dope? – Formal analysis of surreptitiously "enhanced" programs -- Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants -- Confluence of Graph Rewriting with Interfaces -- Verifying Robustness of Event-Driven Asynchronous Programs against Concurrency -- Incremental update for graph rewriting -- Linearity, Control Effects, and Behavioral Types -- Temporary Read-Only Permissions for Separation Logic -- Faster Algorithms for Weighted Recursive State Machines -- ML and Extended BVASS. – Metric Reasoning about Lambda Terms: the General Case -- Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring -- Probabilistic Termination by Monadic Affine Sized Typing -- Caper: Automatic Verification for Fine-grained Concurrency -- Tackling Real-Life Relaxed Concurrency with FSL++. - Extensible Datasort Refinements -- Programs Using Syntax with First-Class Binders. - Lincx: A Linear Logical Framework with First-class Context -- APLicative Programming with Naperian Functors -- Verified Characteristic Formulae for CakeML -- Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic -- Proving Linearizability Using Partial Orders -- The Power of Non-Determinism in Higher-Order Implicit Complexity -- The Essence of Higher-Order Concurrent Separation Logic -- Comprehending Isabelle/HOL’s Consistency.-The essence of functional programming on semantic data -- A Classical Sequent Calculus with Dependent Types -- Context-Free Session Type Inference -- Modular Verification of Higher-order Functional Programs -- Commutative semantics for probabilistic programming -- Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization -- A Higher-Order Logic for Concurrent Termination-Preserving Refinement -- Modular Verification of Procedure Equivalence in the Presence of Memory Allocation -- Abstract Specifications for Concurrent Maps. |
| Record Nr. | UNISA-996466207503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Programming Languages and Systems : 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings / / edited by Hongseok Yang
| Programming Languages and Systems : 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings / / edited by Hongseok Yang |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XV, 992 p. 236 illus.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Compilers (Computer programs)
Computer science Software engineering Computer programming Compilers and Interpreters Computer Science Logic and Foundations of Programming Software Engineering Theory of Computation Programming Techniques |
| ISBN | 3-662-54434-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Disjoint Polymorphism -- Generalizing inference systems by coaxioms -- Observed Communication Semantics for Classical Processes -- Is your software on dope? – Formal analysis of surreptitiously "enhanced" programs -- Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants -- Confluence of Graph Rewriting with Interfaces -- Verifying Robustness of Event-Driven Asynchronous Programs against Concurrency -- Incremental update for graph rewriting -- Linearity, Control Effects, and Behavioral Types -- Temporary Read-Only Permissions for Separation Logic -- Faster Algorithms for Weighted Recursive State Machines -- ML and Extended BVASS. – Metric Reasoning about Lambda Terms: the General Case -- Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring -- Probabilistic Termination by Monadic Affine Sized Typing -- Caper: Automatic Verification for Fine-grained Concurrency -- Tackling Real-Life Relaxed Concurrency with FSL++. - Extensible Datasort Refinements -- Programs Using Syntax with First-Class Binders. - Lincx: A Linear Logical Framework with First-class Context -- APLicative Programming with Naperian Functors -- Verified Characteristic Formulae for CakeML -- Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic -- Proving Linearizability Using Partial Orders -- The Power of Non-Determinism in Higher-Order Implicit Complexity -- The Essence of Higher-Order Concurrent Separation Logic -- Comprehending Isabelle/HOL’s Consistency.-The essence of functional programming on semantic data -- A Classical Sequent Calculus with Dependent Types -- Context-Free Session Type Inference -- Modular Verification of Higher-order Functional Programs -- Commutative semantics for probabilistic programming -- Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization -- A Higher-Order Logic for Concurrent Termination-Preserving Refinement -- Modular Verification of Procedure Equivalence in the Presence of Memory Allocation -- Abstract Specifications for Concurrent Maps. |
| Record Nr. | UNINA-9910483836903321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Programming Languages and Systems [[electronic resource] ] : 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings / / edited by Hongseok Yang
| Programming Languages and Systems [[electronic resource] ] : 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings / / edited by Hongseok Yang |
| Edizione | [1st ed. 2011.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 |
| Descrizione fisica | 1 online resource (XI, 372 p. 114 illus., 6 illus. in color.) |
| Disciplina | 005.13 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Programming languages (Electronic computers)
Software engineering Computer logic Computer security Computer programming Mathematical logic Programming Languages, Compilers, Interpreters Software Engineering Logics and Meanings of Programs Systems and Data Security Programming Techniques Mathematical Logic and Formal Languages |
| ISBN | 3-642-25318-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Title Page -- Preface -- Organization -- Table of Contents -- Invited Talks -- Program Analysis and Machine Learning: A Win-Win Deal -- References -- Software Verification with Liquid Types -- Engineering Theories with Z3 -- Introduction -- SMT, DPLL(T), and Z3 -- SMT -- DPLL(T) -- Z3's Theory Solver API -- Weighted MaxSMT -- Theories for Partial Orders and Class Inheritance -- A Basic Solver for Partial Orders -- Sub-typing Closure -- A Theory of Object Graphs -- An Encoding Using Arrays -- An Encoding Using Recursive Data-Types and Arrays -- Not All Encodings are Equal -- HOL -- Leveraging Theories -- Conclusions -- References -- Algebra, Logic, Locality, Concurrency -- References -- Session 1: Program Analysis -- Modular Abstractions of Reactive Nodes Using Disjunctive Invariants -- Introduction -- Invariants by Predicate Abstraction -- Solution of a Universally Quantified Formula -- Naive Algorithm for a Given Postcondition -- Performance Improvements -- Iterative Refinement of Invariants -- Extensions -- Step-by-Step Example of Invariant Inference -- Construction of the Abstract Automaton -- Related Work -- Conclusion -- Modular Abstractions of Reactive Nodes Using Disjunctive Invariants -- Introduction -- Invariants by Predicate Abstraction -- Solution of a Universally Quantified Formula -- Naive Algorithm for a Given Postcondition -- Performance Improvements -- Iterative Refinement of Invariants -- Extensions -- Step-by-Step Example of Invariant Inference -- Construction of the Abstract Automaton -- Related Work -- Conclusion -- References -- Template-Based Unbounded Time Verification of Affine Hybrid Automata -- Introduction -- Basics -- Our Approach: Getting into the Corset of the Monotone Framework -- Adapting the Max-Strategy Approach -- Conclusion -- References -- Access-Based Localization with Bypassing -- Introduction.
Setting: Analysis Framework -- Graph Representation of Programs -- Static Analysis -- Access-Based Localization with Bypassing -- Access-Based Localization: Previous Approach -- Access-Based Localization with Bypassing: Our Approach -- Delivery Points Optimization -- Experiments -- Setting Up -- Results -- Related Work -- Conclusion -- References -- Session 2: Functional Programming -- A Deductive Database with Datalog and SQL Query Languages -- Introduction -- System Architecture -- Source-to-Source Program Transformations -- Compile-Time Analyses -- Strong Constraints -- Tracing and Debugging -- Conclusions -- References -- Constructing List Homomorphisms from Proofs -- Introduction -- Preliminaries -- Folds and List Homomorphisms -- From Duality to Homomorphism -- The Steep List Problem -- Constructing ( ) Formally -- Computing Capacity by a List Homomorphism -- Parallel Scan -- Reasoning with Conditionals -- Conclusions -- References -- Extending Hindley-Milner Type Inference with Coercive Structural Subtyping -- Introduction -- Notation and Terminology -- Terms and Types -- Subtyping and Coercions -- Type Substitutions and Unification -- Type Inference with Coercions -- Coercive Subtyping Using Subtype Constraints -- Constraint Generation -- Constraint Simplification -- Solving Subtype Constraints on a Graph -- Coercion Insertion -- Total Correctness and Completeness -- An Example for Incompleteness -- Complexity and Completeness -- Related Work -- Conclusion -- References -- Polymorphic Multi-stage Language with Control Effects -- Introduction -- Preliminaries -- Introducing Polymorphism Safely -- The Calculus -- Type System -- Type Soundness -- Principal Type and Type Inference -- Conclusion -- References -- Session 3: Compiler -- Compiler Backend Generation for Application Specific Instruction Set Processors -- Introduction. Design Overview -- Background -- Open64. -- Olive. -- Design Goals -- Design Framework -- OpenDL -- Instruction Description -- Common Information Extraction -- Instruction Sharing -- Pattern Abstraction -- Rule Library -- Terminal Declaration -- Nonterminal Declaration -- Grammar Rules -- Mapping Rules -- AutoAST -- Experimental Results -- OpenDL -- Reliability -- Performance of Embedded Benchmarks -- Performance of Large-Scale Applications -- Case Study: Design Space Exploration of ASIPs -- Related Work -- Conclusion -- References -- A Non-iterative Data-Flow Algorithmfor Computing Liveness Sets in Strict SSA Programs -- Introduction -- Related Work -- Foundations -- Control-Flow Graph and Loop Structure -- Static Single Assignment Form -- Liveness -- Complexity of Liveness Algorithms -- Computing Liveness Sets Using Loop-Nesting Forests -- Liveness Sets on Reducible Control-Flow Graphs -- Liveness Sets on Irreducible Control-Flow Graphs -- Experiments -- Conclusion -- References -- SPAS: Scalable Path-Sensitive Pointer Analysison Full-Sparse SSA -- Introduction -- Related Work -- The Basic Idea -- A Motivating Example -- The SPAS Framework -- Encoding Program Paths as BDDs -- Extended SSA Form -- Capturing Path Correlation -- Supporting Strong Updates -- Experimental Evaluation -- Analysis Overhead -- Path-Sensitive Precision -- Conclusion -- References -- Session 4: Concurrency 1 -- On the Strength of Owicki-Gries for Resources -- Introduction -- Resource-Manipulating Language and Its Semantics -- Language RPL -- Semantics of RPL -- Owicki-Gries-Core Proofs -- Lattice of Owicki-Gries-Core Proofs -- Examples -- Owicki-Gries Core as Abstract Interpretation -- Owicki-Gries-Core Proofs are the Post-Fixpoints of a Sound Abstract Successor Map -- Characteristic Closures for Owicki-Gries Core? -- Absence of Equivalent Characterizations by Closures. Upper Bound on Precision -- Lower Bound on Precision -- Simple Cartesian Closure -- More Precise Lower Bound Closure -- Related Work -- Discussion -- Challenges -- Conclusion -- References -- Solving Recursion-Free Horn Clauses over LI+UIF -- Introduction -- Illustration -- Recursion-Free Horn Clauses -- Algorithm -- Resolution Tree -- Proof Tree -- Annotated Proof Tree -- Correctness and Complexity -- Conclusion -- References -- Macro Tree Transformations of Linear Size Increase Achieve Cost-Optimal Parallelism -- Introduction -- Preliminary -- Trees -- Parallel Tree Contraction -- Tree Transducers -- Macro Tree Transducers -- Strongly Single-Use Restricted MTTs -- Top-Down Relabeling with Regular Lookahead -- Parallel Evaluation of Tree Transformations -- Parallel Evaluation of Top-Down Relabeling with Regular Lookaheads -- Parallel Evaluation of Strongly Single-Use Restricted Macro Tree Transducers -- Parallel Evaluation of Complicated Tree Transformations of Linear Size Increase -- Macro Tree Transformations -- Higher-Order Tree Transformations -- Primitive Recursive Tree Transformations -- Tree-Walking Transformations with Pebbles -- Other Classes of Tree Transformations -- Concluding Remarks -- References -- Decentralized Delimited Release -- Introduction -- Decentralized Delimited Release -- Decentralized Policies -- From DLM0 to Families of Indistinguishability Relations -- Enforcement -- Experiments -- Related Work -- Conclusion -- References -- Session 5: Concurrency 2 -- Cost Analysis of Concurrent OO Programs -- Introduction -- A Language with Concurrent Objects -- A Rule-Based Intermediate Language -- Cost and Cost Models for Concurrent Programs -- The Basic Cost Analysis Framework -- Field-Sensitive Size Analysis for Concurrent OO Programs -- Cost Relations Based on Cost Centers -- Class Invariants in Cost Analysis. Experiments: The COSTABS System -- Conclusions and Related Work -- References -- Static Object Race Detection -- Introduction -- Formal Account of Object Graphs -- Concrete Semantics -- Abstract Semantics -- Dominance Inference Analysis -- Dominance Boundary -- Minimal Boundaries -- Object Race Detection -- Reentrancy Analysis -- Lock Analysis -- Object Race Detection Analysis -- Implementation -- Related Work -- Conclusions -- References -- Soundness of Data Flow Analyses for Weak Memory Models -- Introduction -- Background -- Weak Memory Models -- Programs vs. Event Structures -- Soundness of Analyses on Weak Memory Models -- Definition of Soundness -- SC-Soundness Entails A-Soundness for Non-relational Analyses -- Proving Soundness of Analyses over Programs -- Repairing Unsound Analyses -- Specification vs. Implementations of the Repair Loop -- Related Work and Conclusion -- References -- Session 6: Semantics -- Towards a Certified Petri Net Model-Checker -- Introduction -- Coloured Petri Nets -- LLVM -- Syntax and Intuitive Semantics -- LLVM-Labelled Petri Nets -- Implementing State Space Exploration -- A Formal Semantics of LLVM -- Memory Model -- Inference Rules -- Data Structures Interpretation -- Correctness and Termination Results -- Conclusion -- References -- Elementary Linear Logic Revisited for Polynomial Timeand an Exponential Time Hierarchy -- Introduction -- Characterization of the Classes P and k-EXP -- Proof-Nets and Complexity Soundness -- Extensional Completeness -- Conclusion and Future Work -- References -- A Proof Pearl with the Fan Theorem and Bar Induction -- Introduction -- Preliminaries -- Always Blue and Eventually Red Trees -- Always Blue Trees -- Eventually Red Trees -- Eventually Always vs. Almost Always Blue Trees -- Eventually Always Blue Trees -- Almost Always Blue Trees. Always Eventually Red vs. Infinitely Often Red Trees. |
| Record Nr. | UNISA-996466244603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||