Programming Languages and Systems

ETAPS Foreword
Preface
Organization
Contents
The Decidability of Verification under PS 2.0
	1 Introduction
	2 Preliminaries
	3 The Promising Semantics
	4 Undecidability of Consistent Reachability in PS 2.0
	5 Decidable Fragments of PS 2.0
		5.1 Formal Model of LoHoW
		5.2 Decidability of LoHoW with Bounded Promises
	6 Source to Source Translation
		6.1 Translation Maps
	7 Implementation and Experimental Results
	8 Related Work and Conclusion
	References
Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains
	1 Introduction
		1.1 Motivating Example: Leader election
		1.2 Challenges in property checking
		1.3 Our Contributions
	2 Background and Terminology
		2.1 Modeling of Asynchronous Message Passing Systems as VCFGs
		2.2 Data flow analysis over iVCFGs
	3 Backward DFAS Approach
		3.1 Assumptions and Definitions
		3.2 Properties of Demand and Covering
		3.3 Data Flow Analysis Algorithm
		3.4 Illustration
		3.5 Properties of the algorithm
	4 Forward DFAS Approach
	5 Implementation and Evaluation
		5.1 Benchmarks and modeling
		5.2 Data flow analysis results
		5.3 Limitations and Threats to Validity
	6 Related Work
	7 Conclusions and Future Work
	References
Types for Complexity of Parallel Computation in Pi-Calculus
	1 Introduction
	2 The Pi-calculus with Semantics for Work and Span
		2.1 Syntax, Congruence and Standard Semantics for π-Calculus
		2.2 Semantics and Complexity
		2.3 An Example Process
	3 Size Types for the Work
		3.1 Size Input/Output Types
		3.2 Subject Reduction
	4 Types for Parallel Complexity
		4.1 Size Types with Time
		4.2 Examples
		4.3 Complexity Results
	5 An Example: Bitonic Sort
	6 Related Work
	7 Perspectives
	Acknowledgements
	References
Checking Robustness Between Weak Transactional Consistency Models-5pt
	1 Introduction
	2 Overview
	3 Consistency Models
		3.1 Robustness
	4 Robustness Against CC Relative to PC
	5 Robustness Against PC Relative to SI
	6 Proving Robustness Using Commutativity DependencyGraphs
	7 Experimental Evaluation
	8 Related Work
	References
Verified Software Units
	1 Introduction
	2 Program verification using VST
	3 VSU calculus
		3.1 Components and soundness
		3.2 Derived rules
	4 APDs and specification interfaces
		4.1 Abstract predicate declarations (APDs)
		4.2 Abstract specification interfaces (ASIs)
		4.3 Verification of ASI-specified compilation units
		4.4 A VSU for a malloc-free library
		4.5 Putting it all together
	5 Modular verification of the Subject/Observer pattern
		5.1 Specification and proof reuse
		5.2 Pattern-level specification
	6 Verification of object principles
	7 Discussion
	References
An Automated Deductive Verification Framework for Circuit-building Quantum Programs
	1 Introduction
		1.1 Quantum computing
		1.2 The hybrid model.
		1.3 The problem with quantum algorithms.
		1.4 Goal and challenges.
		1.5 Proposal.
		1.6 Contributions.
		1.7 Discussion.
	2 Background: Quantum Algorithms and Programs
		2.1 Quantum data manipulation.
		2.2 Quantum circuits.
		2.3 Reasoning on circuits and the matrix semantics.
		2.4 Path-sum representation.
	3 Introducing PPS
		3.1 Motivating example.
		3.2 Parametrizing path-sums.
	4 Qbricks-DSL
		4.1 Syntax of Qbricks-DSL.
		4.2 Operational semantics.
		4.3 Properties.
		4.4 Universality and usability of the chosen circuit constructs.
		4.5 Validity of circuits.
		4.6 Denotational semantics.
	5 Qbricks-Spec
		5.1 Syntax of Qbricks-Spec.
		5.2 The types pps and ket.
		5.3 Denotational semantics of the new types.
		5.4 Regular sequents in Qbricks-Spec.
		5.5 Parametricity of PPS.
		5.6 Standard matrix semantics and correctness of PPS semantics.
	6 Reasoning on Quantum Programs
		6.1 HQHL judgments.
		6.2 Deduction rules for term constructs.
		6.3 Deduction rules for pps.
		6.4 Equational reasoning.
		6.5 Additional deductive rules.
	7 Implementation
	8 Case studies and experimental evaluation
		8.1 Examples of formal specifications.
		8.2 Experimental evaluation.
		8.3 Prior verification efforts.
		8.4 Evaluation: benefits of PPS and Qbricks.
	9 Related works
	10 Conclusion
	Acknowledgments.
	References
Nested Session Types
	1 Introduction
	2 Overview of Nested Session Types
	3 Description of Types
	4 Type Equality
		4.1 Type Equality Definition
		4.2 Decidability of Type Equality
	5 Practical Algorithm for Type Equality
		5.1 Type Equality Declarations
	6 Formal Language Description
		6.1 Basic Session Types
		6.2 Type Safety
	7 Relationship to Context-Free Session Types
	8 Implementation
	9 More Examples
	10 Further Related Work
	11 Conclusion
	References
Coupled Relational Symbolic Execution for Differential Privacy
	1 Introduction
	2 CRSE Informally
	3 Preliminaries
	4 Concrete languages
		4.1 PFOR
		4.2 RPFOR
	5 Symbolic languages
		5.1 SPFOR
		5.2 SRPFOR
	6 Metatheory
	7 Strategies for counterexample finding
	8 Examples
	9 Related Works
	10 Conclusion
	References
Graded Hoare Logic and its Categorical Semantics
	1 Introduction
	2 Overview of GHL and Prospectus of its Model
	3 Loop Language and Graded Hoare Logic
		3.1 Preliminaries
		3.2 The Loop Language
		3.3 Assertion Logic
		3.4 Graded Hoare Logic
		3.5 Example Instantiations of GHL
	4 Graded Categories
		4.1 Homogeneous Coproducts in Graded Categories
		4.2 Graded Freyd Categories with Countable Coproducts
		4.3 Semantics of The Loop Language in Freyd Categories
	5 Modelling Graded Hoare Logic
		5.1 Interpretation of the Assertion Logic using Fibrations
		5.2 Interpretation of Graded Hoare Logic
		5.3 Instances of Graded Hoare Logic
	6 Related Work
	7 Conclusion
	References
Do Judge a Test by its Cover
	1 Introduction
	2 Classical Combinatorial Testing
	3 Generalizing Coverage
	4 Sparse Test Descriptions
		4.1 Encoding “Eventually”
		4.2 Defining Coverage
	5 Thinning Generators with QuickCover
		5.1 Online Generator Thinning
	6 Evaluation
		6.1 Case Study: Normalization Bugs in System F
		6.2 Case Study: Strictness Analysis Bugs in GHC
	7 Related Work
		7.1 Generalizations of Combinatorial Testing
		7.2 Comparison with Enumerative Property-Based Testing
		7.3 Comparison with Fuzzing Techniques
	8 Conclusion and Future Work
		8.1 Variations
		8.2 Combinatorial Coverage of More Types
		8.3 Regular Tree Expressions for Directed Generation
		Acknowledgments
		References
For a Few Dollars More
	1 Introduction
	2 Specification of Algorithms With Resources
		2.1 Nondeterministic Computations With Resources
		2.2 Atomic Operations and Control Flow
		2.3 Refinement on NREST
		2.4 Refinement Patterns
	3 LLVM With Cost Semantics
		3.1 Basic Monad
		3.2 Shallowly Embedded LLVM Semantics
		3.3 Cost Model
		3.4 Reasoning Setup
		3.5 Primitive Setup
	4 Automatic Refinement
		4.1 Heap nondeterminism refinement
		4.2 The Sepref Tool
		4.3 Extracting Hoare Triples
		4.4 Attain Supremum
	5 Case Study: Introsort
		5.1 Specification of Sorting
		5.2 Introsort’s Idea
		5.3 Quicksort Scheme
		5.4 Final Insertion Sort
		5.5 Separating Correctness and Complexity Proofs
		5.6 Refining to LLVM
		5.7 Benchmarks
	6 Conclusions
		6.1 Related Work
		6.2 Future Work
	References
Run-time Complexity Bounds Using Squeezers
	1 Introduction
	2 Overview
	3 Complexity Analysis based on Squeezers
		3.1 Time complexity as a function of rank
		3.2 Complexity decomposition by partitioned simulation
		3.3 Extraction of recurrence relations over ranks
		3.4 Establishing the requirements of the recurrence relations extraction
		3.5 Trace-length vs. state-size recurrences with squeezers
	4 Synthesis
		4.1 SyGuS
		4.2 Verification
	5 Empirical Evaluation
		5.1 Experiments
		5.2 Case study: Subsets example
	6 Related Work
	7 Conclusion
	Acknowledgements.
	References
Complete trace models of state and control
	1 Introduction
	2 HOSC
	3 HOSC[HOSC]
		3.1 Names and abstract values
		3.2 Actions and traces
		3.3 Extended syntax and reduction
		3.4 Configurations
		3.5 Transitions
		3.6 Correctness and full abstraction
	4 GOSC[HOSC]
	5 HOS[HOSC]
	6 GOS[HOSC]
	7 Concluding remarks
	8 Related Work
	References
Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols
	1 Introduction
	2 Session Types
	3 Session Coalgebra
		3.1 Alternative Presentation of Session Coalgebras
		3.2 Coalgebra of Session Types
	4 Type Equivalence, Duality and Subtyping
		4.1 Bisimulation
		4.2 Duality
		4.3 Parallelizability
		4.4 Simulation and Subtyping
		4.5 Decidability
	5 Typing Rules
		5.1 A Session π-calculus
		5.2 Typing Rules
	6 Algorithmic Type Checking
	7 Concluding Remarks
	References
Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages
	1 Introduction
	2 A Motivating Example from Phylogenetics
	3 A Calculus for Probabilistic Programming Languages
		3.1 Syntax
		3.2 Semantics
		3.3 Resampling Semantics
	4 The Target Measure of a Program
		4.1 A Measure Space over Traces
		4.2 A Measurable Space over Terms
	5 Formal SMC
		5.1 Preliminaries: Transition Kernels
		5.2 Algorithm
		5.3 Correctness
	6 Formal SMC for Probabilistic Programming Languages
		6.1 The Sequence of Measures Generated by a Program
		6.2 Correctness
	7 SMC Algorithms
		7.1 The Bootstrap Particle Filter
		7.2 Other SMC Algorithms
	8 Related Work
	9 Conclusions
	Acknowledgments
	References
Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere
	1 Introduction
	2 Probabilistic Programming and Trace-Based Inference
		2.1 Measures and Densities
		2.2 Probabilistic Programming: a (Running) Example
		2.3 Gradient-Based Approximate Inference
	3 Sampling Semantics for Statistical PCF
		3.1 Statistical PCF
		3.2 Operational Semantics
	4 Differentiability of the Weight and Value Functions
		4.1 Background on Differentiable Functions
		4.2 Why Almost Everywhere Differentiability Can Fail
		4.3 Admissible Primitive Functions
		4.4 Almost Sure Termination
	5 Stochastic Symbolic Execution
		5.1 Symbolic Terms and Values
		5.2 Symbolic Operational Semantics
	6 Densities of Almost Surely Terminating Programs areDifferentiable Almost Everywhere
		6.1 Differentiability on Terminating Traces
		6.2 Differentiability for Almost Surely Terminating Terms
	7 Conclusion
	References
Graded Modal Dependent Type Theory
	1 Introduction
	2 GrTT: Graded Modal Dependent Type Theory
		2.1 Syntax
		2.2 Typing Judgments, Contexts, and Grading
		2.3 Typing Rules
		2.4 Operational Semantics
		2.5 Implementation and Examples
	3 Case Studies
		3.1 Recovering Martin-L¨of Type Theory
		3.2 Determining Usage via Quantitative Semirings
		3.3 Simply-typed Reasoning
		3.4 Recovering Parametricity via Grading
		3.5 Graded Modal Types and Non-dependent Linear Types
	4 Metatheory
		4.1 Substitution
		4.2 Type Preservation
		4.3 Structural Rules
		4.4 Strong Normalization
	5 Implementation
	6 Discussion
	References
Automated Termination Analysis of Polynomial Probabilistic Programs
	1 Introduction
	2 Preliminaries
		2.1 Programming Model: Prob-Solvable Loops
		2.2 Canonical Probability Space
		2.3 Martingales
	3 Proof Rules for Probabilistic Termination
		3.1 Positive Almost Sure Termination (PAST)
		3.2 Almost Sure Termination (AST)
		3.3 Non-Termination
	4 Relaxed Proof Rules for Probabilistic Termination
	5 Algorithmic Termination Analysis through Asymptotic Bounds
		5.1 Prob-solvable Loops and Monomials
		5.2 Computing Asymptotic Bounds for Prob-solvable Loops
		5.3 Algorithms for Termination Analysis of Prob-solvable Loops
		5.4 Ruling out Proof Rules for Prob-Solvable Loops
	6 Implementation and Evaluation
		6.1 Implementation
		6.2 Experimental Setting and Results
	7 RelatedWork
	8 Conclusion
Bayesian strategies: probabilistic programs as generalised graphical models
	1 Introduction
		1.1 From Bayesian networks to Bayesian strategies
		1.2 Our approach
	2 Probability distributions, Bayesian networks, andprobabilistic programming
		2.1 Probability and measure
		2.2 Bayesian networks
		2.3 A language for probabilistic modelling
	3 Programs as event structures
		3.1 Control flow, data flow, and probability
		3.2 Branching
		3.3 Programs with free variables
		3.4 Higher-order programs
		3.5 Bayesian event structures
		3.6 Symmetry
	4 Games and Bayesian strategies
		4.1 An introduction to game semantics based on event structures
		4.2 Composition of strategies
	5 A denotational model
		5.1 Categorical structure
		5.2 Denotational semantics
	6 Conclusion and perspectives
	References
Temporal Refinements for Guarded Recursive Types
	1 Introduction
	2 Outline
	3 The Pure Calculus
	4 A Temporal Modal Logic
	5 A Temporally Refined Type System
	6 The Full System
	7 Semantics
	8 Examples
	9 Related Work
	10 Conclusion and Future Work
	References
Query Lifting
	1 Introduction
	2 Overview
	3 Background
	4 A relational calculus of tabular functions
		4.1 Semantics and translation to NRCλ(Set, Bag)
	5 Delateralization
	6 Query lifting and shredding
		6.1 Reflecting shredded queries into NRCλ(Set, Bag)
		6.2 The stitching function
	7 Related work
	8 Conclusions
	References
Reverse AD at Higher Types: Pure, Principled and Denotationally Correct
	1 Introduction
	2 Key Ideas
	3 λ-Calculus as a Source Language for AD
	4 Linear λ-Calculus as an Idealised AD Target Language
	5 Semantics of the Source and Target Languages
		5.1 Preliminaries
		5.2 Abstract Semantics
		5.3 Concrete Semantics
	6 Pairing Primals with Tangents/Adjoints, Categorically
		6.1 Grothendieck Constructions on Strictly Indexed Categories
		6.2 Structure of ΣCL and ΣCLop for Locally Indexed Categories
	7 Novel AD Algorithms as Source-Code Transformations
	8 Proving Reverse and Forward AD Semantically Correct
		8.1 Preliminaries
		8.2 Subsconing for Correctness of AD
	9 Practical Relevance and Implementation
	10 Related and Future Work
	Acknowledgements
	References
Sound and Complete Concolic Testingfor Higher-order Functions
	1 Introduction
	2 Higher-order Concolic Testing by Example
		2.1 First-Order Concolic Execution in a Nutshell
		2.2 From Numbers to Function Inputs
		2.3 Input Interactions
		2.4 Blind Extensions Are Not Enough
		2.5 Higher-order Inputs
	3 Formalizing Higher-order Concolic Testing
		3.1 From User Programs to Concolic Evaluation
		3.2 Evolution of Higher-order Inputs
		3.3 Adding Concretization
	4 Correctness of Higher-order Concolic Testing
	5 From the Model to a Proof-of-Concept Implementation
	6 Related Work
	7 Conclusion
	Acknowledgments
	References
Strong-Separation Logic
	1 Introduction
	2 Strong- and Weak-Separation Logic
		2.1 Preliminaries
		2.2 Two Semantics of Separation Logic
		2.3 Correspondence of Strong and Weak Semantics on Positive Formulas
	3 Deciding the SSL Satisfiability Problem
		3.1 Memory Chunks
		3.2 Abstract Memory States
		3.3 The Refinement Theorem for SSL
		3.4 Recursive Equations for Abstract Memory States
		3.5 Refining the Refinement Theorem: Bounding Garbage
		3.6 Deciding SSL by AMS Computation
		3.7 Complexity of the SSL Satisfiability Problem
	4 Program Verification with Strong-Separation Logic
	5 Normal Forms and the Abduction Problem
	6 Conclusion
	References
Author Index