
Programming Languages and Systems
Description
Alles über E-Books | Antworten auf Fragen rund um E-Books, Kopierschutz und Dateiformate finden Sie in unserem Info- & Hilfebereich.
More details
Other editions
Additional editions

Content
- Intro
- Preface
- Organization
- Invited Talks
- Programming with "Big Code"
- Analyzing JavaScript Web Applications in the Wild (Mostly) Statically
- Probabilistic Programming
- Contents
- Invited Talk
- Programming with ``Big Code''
- References
- Compilers
- Memory-Efficient Tail Calls in the JVM with Imperative Functional Objects
- 1 Introduction
- 2 FCore and IFOs, Informally
- 2.1 Encoding Functions with IFOs
- 2.2 Tail-Call Elimination
- 3 Compiling FCore
- 4 Tail-Call Elimination
- 5 Implementation and Evaluation
- 5.1 Implementation
- 5.2 Evaluation
- 6 Related Work
- 7 Conclusion and Future Work
- References
- A Secure Compiler for ML Modules
- 1 Introduction
- 2 Overview
- 2.1 The Source Language ModuleML
- 2.2 The Low-Level Target Language A+I
- 2.3 The Attacker
- 2.4 The Secure Abstract Data Type Pattern
- 3 A Secure Compiler for ModuleML
- 3.1 Booleans, Integers and Pairs
- 3.2 Abstract Types
- 3.3 Structures and Signatures
- 3.4 Higher-Order Functions
- 3.5 Locations
- 3.6 Functors
- 4 Compiler Reflection
- 5 Implementation and Experimental Results
- 6 Related Work
- 7 Conclusions
- References
- Detection of Redundant Expressions: A Complete and Polynomial-Time Algorithm in SSA
- 1 Introduction
- 2 Motivation
- 2.1 Kildall's Algorithm
- 2.2 Gulwani's Algorithm
- 2.3 Our View
- 3 Terminology
- 4 Basic Concept
- 4.1 Value -function
- 4.2 Proposed Method
- 5 Algorithm
- 5.1 Join
- 5.2 Transfer Function
- 5.3 The Iterative Algorithm
- 5.4 Complexity Analysis
- 6 Implementation and Results
- 7 Related Work
- 8 Conclusion
- References
- Separation Logic
- Separation Logic with Monadic Inductive Definitions and Implicit Existentials
- 1 Introduction
- 2 Separation Logic with Inductive Definitions
- 2.1 Symbolic Heaps with Inductive Definitions
- 2.2 Implicit Existential
- 2.3 Separation Logic Sep
- 2.4 Semantics
- 2.5 Related Work
- 2.6 Main Ideas
- 3 Translation in Sep
- 3.1 Transformation of Weak Progress into Progress
- 3.2 Simplification of Definition Clauses
- 3.3 Separation Logic Sep
- 3.4 Translation of Inductive Predicates in Sep
- 3.5 Translation of Symbolic Heaps in Sep
- 4 Translation in Bounded-Treewidth Separation Logic
- 5 Main Theorems
- 6 Undecidability of SLRDbtw with Implicit Existentials
- 7 Conclusion
- References
- Tree-Like Grammars and Separation Logic
- 1 Introduction
- 2 Preliminaries
- 3 Context-Free Graph Grammars
- 4 Tree-Like Grammars
- 5 Tree-Like Separation Logic
- 6 Conclusion
- References
- Static Analysis and Abstract Interpretation
- Randomized Resource-Aware Path-Sensitive Static Analysis
- 1 Introduction
- 1.1 Motivating Examples
- 1.2 Trace Hashing
- 1.3 Paper Structure and Contributions
- 2 Trace Hashing as Abstract Interpretation
- 2.1 Basic Definitions and Concrete Semantics
- 2.2 Assumptions About Underlying Analysis
- 2.3 Path-Sensitive Abstract Domain
- 2.4 Hash Update
- 3 The Hash Function Family
- 4 Implementation and Experimental Results
- 4.1 Benchmarking Methodology
- 4.2 Results
- 5 Related Work
- 6 Extensions and Future Work
- References
- Quadratic Zonotopes
- 1 Affine Arithmetics and Static Analysis
- 2 Affine and Quadratic Arithmetics
- 3 Quadratic Zonotopes: A Zonotopic Extension of Quadratic Forms to Environments
- 4 Floating Point Computations
- 5 Improving Concretization Using SDP
- 6 Experimentation
- 7 Conclusion
- References
- Abstraction of Optional Numerical Values
- 1 Introduction
- 2 Overview
- 3 A Language with Optional Values and Its Semantics
- 4 Abstraction in Presence of Optional Numerical Values
- 5 Application to Numerical Domains Based on Linear Inequalities
- 5.1 The Bi-Avatar Strategy
- 5.2 Condition Test
- 5.3 Verifying the Satisfaction of a Constraint
- 5.4 Assignment
- 5.5 Inclusion Checking, Join and Widening
- 5.6 Analysis
- 6 Possibly Empty Summary Variables
- 7 Implementation and Examples
- 8 Related Works
- 9 Conclusion
- References
- Hoare Logic and Types
- Fault-Tolerant Resource Reasoning
- 1 Introduction
- 2 Motivating Examples
- 2.1 Naive Bank Transfer
- 2.2 Fault-Tolerant Bank Transfer: Implementation
- 2.3 Fault-Tolerant Bank Transfer: Verification
- 3 Program Logic
- 3.1 Example: Concurrent Bank Transfer
- 4 Case Study: ARIES
- 5 Semantics and Soundness
- 5.1 Fault-Tolerant Views
- 5.2 Fault-Tolerant Concurrent Separation Logic
- 6 Related Work
- 7 Conclusions and Future Work
- References
- Shifting the Blame
- 1 Introduction
- 2 Blame Calculus with Shift and Reset
- 2.1 Blame Calculus
- 2.2 Delimited-Control Operators: Shift and Reset
- 2.3 Blame Calculus with Shift and Reset
- 3 Language
- 3.1 Syntax
- 3.2 Semantics
- 3.3 Type System
- 3.4 Type Soundness
- 4 Blame Theorem
- 4.1 Subtyping
- 4.2 Blame Theorem
- 5 CPS Transformation
- 6 Related Work
- 7 Conclusion
- References
- Aliasing Control in an Imperative Pure Calculus
- 1 Introduction
- 2 Syntax and Type System
- 3 Examples
- 4 Calculus
- 5 Results
- 6 Related Work
- 7 Conclusion
- References
- Functional Programming and Semantics
- A Strong Distillery
- 1 Introduction
- 2 Linear Leftmost-Outermost Reduction
- 3 Distilleries
- 4 Strengthening the MAM
- 5 The Strong Milner Abstract Machine
- 6 Distilling the Strong MAM
- 7 Complexity Analysis
- References
- From Call-by-Value to Interaction by Typed Closure Conversion
- 1 Introduction
- 2 Source Language
- 3 Target Language
- 3.1 Equational Theory
- 4 Translation
- 4.1 Examples
- 5 Correctness
- 5.1 Lower Bound
- 5.2 Upper Bound
- 6 Conclusion and Further Work
- References
- Kripke Open Bisimulation
- 1 Introduction
- 2 RefML
- 2.1 Syntax of RefML
- 2.2 Operational Semantics
- 2.3 Abstract Values and Nominal Reasoning
- 3 Trace Semantics
- 3.1 Interactive Reduction
- 3.2 Nominal Equivalence of Traces
- 3.3 A Simple Bisimulation on Traces
- 4 Kripke Open Bisimulations
- 4.1 Transition Systems and Worlds
- 4.2 Definition of KOBs
- 4.3 An Example: Well-Bracketed State Change
- 5 Soundness
- 6 Completeness
- 6.1 Faithful Kripke Bisimulations on Traces
- 6.2 Exhaustive WTS
- 7 Future Work
- References
- Model Checking
- Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs
- 1 Introduction
- 2 Preliminaries
- 3 The Verification Problem
- 4 Automata-Based Abstraction
- 4.1 Abstract Programs
- 4.2 Abstraction Method
- 5 Abstraction Refinement
- 5.1 Feasibility Check
- 5.2 Abstraction Refinement
- 6 Implementation and Experiments
- 7 Related Work
- 8 Conclusion
- References
- Decision Algorithms for Checking Definability of Order-2 Finitary PCF
- 1 Introduction
- 2 Preliminaries
- 2.1 Finitary PCF
- 2.2 FPCF Definability Problem
- 3 Algorithm Using Sieber's Relation
- 3.1 Logical Relation
- 3.2 Characterization of Definability
- 3.3 Algorithm
- 3.4 Complexity
- 4 Saturation-Based Algorithm Using Finite Canonical Forms
- 4.1 Finite Canonical Forms of FPCF
- 4.2 Algorithm
- 4.3 Complexity
- 5 Application to Program Equivalence Checking
- 5.1 Observational Equivalence Problem
- 5.2 Algorithm for the Equivalence Problem
- 6 Related Work
- 7 Conclusion
- References
- Program Analysis - I
- Uncovering JavaScript Performance Code Smells Relevant to Type Mutations
- 1 Introduction
- 2 Types in Type-Feedback JavaScript Engine
- 2.1 Type Collection
- 2.2 Type Mutations
- 2.3 Why Type Mutations Impair Performance
- 3 Type Mutation Code Patterns in Practice
- 4 Finding Unintentional Type Mutations
- 4.1 Modeling Type Evolutions
- 4.2 Checking Type Homogeneity
- 4.3 Inferring the Reason of Deoptimization
- 5 Evaluation
- 5.1 Overall Results Discussion
- 5.2 Case Studies for Octane
- 6 Related Work
- 7 Conclusion and Future Work
- References
- Analyzing Distributed Multi-platform Java and Android Applications with ShadowVM
- 1 Introduction
- 2 ShadowVM Overview
- 3 Code Coverage Analysis with ShadowVM
- 4 Fuzzing a Distributed Multi-platform Application
- 5 Related Work
- 6 Conclusions
- References
- Medley
- Quasi-Linearizability is Undecidable
- 1 Introduction
- 2 Concurrent Systems
- 2.1 Notations
- 2.2 Libraries and the Most General Clients
- 2.3 Operational Semantics of Concurrent Systems
- 3 Linearizability and Quasi-Linearizability
- 3.1 Linearizability
- 3.2 Quasi-Linearizability
- 4 Undecidability of Quasi-Linearizability
- 4.1 k-Counter Machine
- 4.2 Libraries for Prefix Closed Regular Languages
- 4.3 Reducing a k-Z Decision Problem to a Linearizability Problem
- 4.4 Undecidability of Quasi-Linearizability
- 5 Conclusion and Future Work
- References
- Objects in Polynomial Time
- 1 Object Oriented Programs
- 1.1 Abstract Syntax
- 1.2 Informal Semantics
- 1.3 Input and Size
- 2 Type System
- 2.1 Tiered Types
- 2.2 Typing Environments and Judgments
- 2.3 Typing Rules
- 2.4 Well-Typedness
- 2.5 Type System Non-Interference Properties
- 3 Safe Recursion
- 3.1 Level and Intricacy
- 3.2 Safety Restriction
- 4 Boolean Lists as an Illustrating Example
- 5 Characterization of Polynomial Time
- 5.1 Polynomial Time Soundness
- 5.2 Polynomial Time Completeness
- 5.3 Decidability of Type Inference
- 6 Methodology of the Presented Analysis
- 7 Expressivity and Open Issues
- References
- Programming Models
- Programming Techniques for Reversible Comparison Sorts
- 1 Introduction
- 2 Preliminaries
- 2.1 Reversible Simulations
- 2.2 The Janus Reversible Programming Language
- 3 Comparison Sorts
- 3.1 Bubble Sort
- 3.2 Insertion Sort
- 3.3 Hygienic Bubble Sort
- 3.4 Selection Sort
- 3.5 Merge Sort
- 3.6 Quicksort
- 4 Concluding Remarks
- A Converting Between Permutation Representations
- References
- Transactions on Mergeable Objects
- 1 Introduction
- 2 Mergeable Objects
- 3 Mergeable Transactions
- 3.1 Operational Semantics of MTM
- 3.2 Properties of MTM
- 3.3 Algorithm
- 4 MTM in Haskell
- 5 Evaluation
- 6 Related Work
- 7 Conclusion
- References
- A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers
- 1 Introduction
- 2 Language Constructs of Safe JCop
- 2.1 Layers and Partial Methods
- 2.2 Layer Activation and First-Class Layers
- 2.3 Dependencies Between Layers
- 2.4 Layer Inheritance
- 2.5 Layer Swapping and Deactivation
- 3 ContextFJ&:
- 3.1 Syntax
- 3.2 Operational Semantics
- 3.3 Type System
- 3.4 Type Soundness
- 4 Related Work
- 5 Concluding Remarks
- References
- Program Analysis - II
- Bottom-Up Context-Sensitive Pointer Analysis for Java
- 1 Introduction
- 2 Example
- 3 Conceptual Foundations
- 3.1 Normalization of Abstract Heaps
- 3.2 Summary-Based Pointer Analysis
- 4 Formalization of Algorithm
- 4.1 Abstract Domains
- 4.2 Operations on Abstract Domains
- 4.3 Intraprocedural Analysis
- 4.4 Interprocedural Analysis
- 5 Implementation and Extensions
- 6 Evaluation
- 7 Related Work
- 8 Conclusion
- References
- More Sound Static Handling of Java Reflection
- 1 Introduction
- 2 Background: Joint Reflection and Points-To Analysis
- 3 Techniques for Empirical Soundness
- 3.1 Generalizing Reflection Inference via Substring Analysis
- 3.2 Use-Based Reflection Analysis
- 3.3 Balancing for Scalability
- 4 Evaluation
- 5 Related Work
- 6 Conclusions
- References
- Author Index
System requirements
File format: PDF
Copy protection: Watermark-DRM (Digital Rights Management)
System requirements:
- Computer (Windows; MacOS X; Linux): Use the free software Adobe Reader, Adobe Digital Editions, or any other PDF viewer of your choice (see eBook Help).
- Tablet/Smartphone (Android; iOS): Install the free app Adobe Digital Editions or another reading app for eBooks, e.g., PocketBook (see eBook Help).
- E-reader: Bookeen, Kobo, Pocketbook, Sony, Tolino and many more (only limited: Kindle).
The file format PDF always displays a book page identically on any hardware. This makes PDF suitable for complex layouts such as those used in textbooks and reference books (images, tables, columns, footnotes). Unfortunately, on the small screens of e-readers or smartphones, PDFs are rather annoying, requiring too much scrolling.
This eBook uses Watermark-DRM, a „soft” copy protection. This means that there are no technical restrictions to prevent illegal distribution. However, there is a personalised watermark embedded in the eBook that can be used to identify the purchaser of the eBook in the event of misuse and to provide evidence for legal purposes.
For more information, see our eBook Help page.