Programming Languages and Systems

Name: Programming Languages and Systems | 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings

Xinyu Feng Sungwoo Park(Editor)

Springer (Publisher)

Published on 8. December 2015

XIX, 506 pages

E-Book

PDF with digital watermarking

System requirements

978-3-319-26529-2 (ISBN)

€53.49incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other 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

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Programming Languages and Systems

Description

More details

Other editions

Additional editions

Content

System requirements