Cover Image

Programming Languages and Systems : 31st European Symposium on Programming, ESOP 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings.

Bibliographic Details
Main Author: Sergey, Ilya.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2022.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
Table of Contents:
  • Intro
  • ETAPS Foreword
  • Preface
  • Organization
  • Contents
  • Categorical Foundations of Gradient-Based Learning
  • 1 Introduction
  • 2 Categorical Toolkit
  • 2.1 Parametric Maps
  • 2.2 Lenses
  • 2.3 Parametric Lenses
  • 2.4 Cartesian Reverse Differential Categories
  • 3 Components of learning as Parametric Lenses
  • 3.1 Models as Parametric Lenses
  • 3.1 Models as Parametric Lenses
  • 3.2 Loss Maps as Parametric Lenses
  • 3.3 Learning Rates as Parametric Lenses
  • 3.4 Optimisers as Reparameterisations
  • 4 Learning with Parametric Lenses
  • 4.1 Supervised Learning of Parameters
  • 4.2 Deep Dreaming: Supervised Learning of Inputs
  • 5 Implementation
  • 5.1 Constructing a Model with Lens and Para
  • 5.2 Learning
  • 6 Related Work
  • 7 Conclusions and Future Directions
  • References
  • Compiling Universal Probabilistic Programming Languages with Efficient Parallel Sequential Monte Carlo Inference
  • 1 Introduction
  • 2 Miking CorePPL
  • 2.1 Design Considerations
  • 2.2 Syntax and Semantics
  • 3 PPL control-flow graphs and RootPPL
  • 3.1 PPL Control-Flow Graphs
  • 3.2 SMC and PCFGs
  • 3.3 RootPPL
  • 4 Compiling to PCFGs
  • 4.1 Function Decomposition Example
  • 4.2 Function Decomposition Algorithm
  • 4.3 CorePPL-to-RootPPL Compiler
  • 4.4 Compiler Strengths and Limitations
  • 5 Evaluation
  • 5.1 Experiment: Constant-Rate Birth Death
  • 5.2 Experiment: Vector-Borne Disease
  • 5.3 Experiment: CRBD with Variance-Reducing Techniques
  • 6 Related Work
  • 7 Conclusion
  • References
  • Foundations for Entailment Checking in Quantitative Separation Logic
  • 1 Introduction
  • 2 (Quantitative) Separation Logic
  • 2.1 Program States
  • 2.2 Separation Logic
  • 2.3 Quantitative Separation Logic
  • 3 Entailments in Probabilistic Program Verification
  • 3.1 Heap-manipulating pGCL
  • 3.2 Weakest Liberal Preexpectations
  • 3.3 Interfered Swap.
  • 3.4 Avoiding Magic Wands
  • 3.5 Randomized List Population
  • 4 Quantitative Entailment Checking
  • 4.1 Idea and Key Observations
  • 4.2 Constructing Finite Overapproximations of Eval (f)
  • 4.3 Lower Bounding QSL [A] by SL [A] Formulae
  • 5 Complexity
  • 6 Application: Decidable hpGCL Verification
  • 6.1 Quantitative Symbolic Heaps
  • 7 Related Work
  • 8 Discussion and Conclusion
  • References
  • Extracting total Amb programs from proofs
  • 1 Introduction
  • 2 Denotational semantics of globally angelic choice
  • 2.1 Programs and types
  • 2.2 Denotational semantics
  • 3 Operational semantics
  • 3.1 Reduction to weak head normal form
  • 3.2 Making choices
  • 3.3 Computational adequacy: Matching denotational and operational semantics
  • 4 CFP (Concurrent Fixed Point Logic)
  • 4.1 Syntax
  • 4.2 Proof rules
  • 4.3 Tarskian semantics, axioms and classical logic
  • 5 Program extraction
  • 5.1 Realizability
  • 5.2 Partial correctness and concurrency
  • 5.3 Soundness and program extraction
  • 6 Application
  • 7 Implementation
  • 8 Conclusion
  • 8.1 Related work
  • 8.2 Modelling locally angelic choice
  • 8.3 Markov's principle with restriction
  • 8.4 Further directions for research
  • References
  • Why3-do: The Way of Harmonious Distributed System Proofs
  • 1 Introduction
  • 2 The Why3 Languages in a Nutshell
  • 3 Distributed Systems and Models
  • 4 The Basic Message-Passing Model
  • 5 Trace Specifications
  • 6 Locally Shared Memory Model
  • 7 Related Work
  • 8 Conclusion
  • References
  • Relaxed virtual memory in Armv8-A
  • 1 Introduction
  • 2 Background: A Crash Course on Virtual Memory
  • 2.1 Virtualising addressing
  • 2.2 The translation-table walk
  • 2.3 Multiple stages of translation
  • 2.4 Caching translations in TLBs
  • 3 Concurrency Architecture Design Questions
  • 3.1 Coherence with respect to physical or virtual addresses.
  • 3.2 Relaxed behaviour from TLB caching
  • 3.3 Relaxed behaviour of translation-walk non-TLB reads
  • 3.4 Further issues
  • 4 Virtual memory in the pKVM production hypervisor
  • 5 Model
  • 6 Tooling
  • 6.1 Isla-based model evaluation
  • 6.2 Experimental testing of hardware
  • 7 Related work
  • 8 Acknowledgments
  • References
  • Verified Security for the Morello Capability-enhanced Prototype Arm Architecture
  • 1 Introduction
  • 2 Overview of the Morello CHERI Architecture
  • 2.1 CHERI Capabilities on Morello
  • 2.2 Capabilities in Registers and Memory
  • 2.3 Capability-aware Instructions
  • 2.4 Domain Transition
  • 2.5 Exceptions and the Memory Management Unit
  • 2.6 Using CHERI in Software
  • 3 Concrete Semantics of Morello
  • 4 Abstract Formal Model of Capability Monotonicity
  • 4.1 ISA Abstraction
  • 4.2 CHERI ISA Parameters
  • 4.3 Capability Abstraction
  • 4.4 CHERI ISA Intra-instruction Properties
  • 4.5 Capability Monotonicity Theorem
  • 5 Proof of Capability Monotonicity in Morello
  • 5.1 Instantiation of the Abstract Model
  • 5.2 Manual Proofs about Capability Encoding Functions
  • 5.3 Proof Engineering
  • 5.4 Bugs and Issues Found
  • 6 Validating the Concrete Semantics
  • 7 Model-based Test Generation
  • 8 Related Work
  • References
  • The Trusted Computing Base of the CompCert Verified Compiler
  • 1 Introduction
  • 2 The Coq Proof Assistant
  • 2.1 Issues in Coq Proof Checking
  • 2.2 Issues in Coq Extraction
  • 3 Use of Axioms in Coq
  • 3.1 Logical Inconsistency
  • 3.2 Mismatches between Coq and OCaml
  • 3.3 Interfacing External Code as Pure Functions
  • 3.4 Pointer Equality and Hash-Consing
  • 4 Front-end and semantic issues
  • 5 Assembly back-end issues
  • 5.1 Printing Issues
  • 5.2 Pseudo-Instructions
  • 5.3 Microarchitectural Concerns
  • 5.4 Assembling and Linking
  • 6 Modeling and Application Binary Interface Issues.
  • 6.1 Modeling of Values
  • 6.2 Foreign Function Interface
  • 6.3 Runtime System
  • 7 Insights and Conclusion
  • References
  • View-Based Owicki-Gries Reasoning for Persistent x86-TSO
  • 1 Introduction
  • 2 Overview and Motivation
  • 2.1 Px86view at a Glance
  • 2.2 PIEROGI: View-Based Owicki-Gries Reasoning for Px86view
  • 3 The PIEROGI Proof rules and Reasoning Principles
  • 3.1 The PIEROGI Programming Language
  • 3.2 View-Based Expressions
  • 3.3 Owicki-Gries Reasoning
  • 3.4 PIEROGI Proof rules
  • 4 Examples
  • 5 PIEROGI Soundness
  • 5.1 The Px86view Model
  • 5.2 The Semantics of PIEROGI Assertions
  • 5.3 Soundness of PIEROGI
  • 6 Mechanisation
  • 7 Related Work
  • References
  • Abstraction for Crash-Resilient Objects
  • 1 Introduction
  • 2 Key Challenges and Ideas
  • 2.1 Library Specifications
  • 2.2 Client-Library Interaction Using Explicit Persist Instructions
  • 2.3 Handling Calling Policies
  • 3 NVM Programs: Syntax and Semantics
  • 3.1 Program Syntax
  • 3.2 Program Semantics
  • 4 The PSC Memory System
  • 4.1 Linking Programs and Memories
  • 4.2 Extending PSC for Library Abstraction
  • 4.3 Separation Properties
  • 5 Libraries and Their Clients
  • 6 The Library Abstraction Theorem
  • 7 An Application: Persistent Pairs
  • 8 Related and Future Work
  • References
  • Static Race Detection for Periodic Programs
  • 1 Introduction
  • 2 Overview
  • 3 Periodic Programs
  • 4 Data Races
  • 5 Response Time and its Computation
  • 5.1 Computing Response time without Locks
  • 6 Rules for Disjointness
  • 6.1 Disjoint Block Rules
  • 6.2 Computing the value m in Rule 5
  • 6.3 Race Detection Algorithm
  • 7 Experimental Evaluation
  • 7.1 Implementation
  • 7.2 Benchmarks
  • 7.3 Results
  • 8 Related Work
  • 9 Conclusion
  • References
  • Probabilistic Total Store Ordering
  • 1 Introduction
  • 2 Preliminaries
  • 3 Concurrent Programs
  • 4 Operational Semantics.
  • 4.1 Configurations
  • 4.2 The Classical TSO Semantics
  • 4.3 Adding Probabilities: PTSO
  • 5 PTSO: Concepts and Properties
  • 5.1 Left-Orientedness and Attractors
  • 6 Qualitative (Repeated) Reachability
  • 6.1 Almost-Sure Reachability
  • 6.2 Almost-Sure Repeated Reachability
  • 6.3 Almost-Never (Repeated) Reachability
  • 6.4 Decidability and Complexity
  • 7 Quantitative (Repeated) Reachability
  • 7.1 Approximate Quantitative Reachability
  • 7.2 Approximate Quantitative Repeated Reachability
  • 8 Expected Average Costs
  • 8.1 Computing costs over runs
  • 8.2 Eagerness
  • 8.3 The Algorithm
  • 9 Conclusions, Discussions, and Perspectives
  • References
  • Linearity and Uniqueness: An Entente Cordiale
  • 1 Introduction
  • 2 Key Ideas
  • 2.1 Are linearity and uniqueness (essentially) the same?
  • 2.2 Are linearity and uniqueness dual?
  • 3 The Linear-Cartesian-Unique Calculus
  • 3.1 Typing
  • 3.2 Equational theory
  • 3.3 Exploiting uniqueness for mutation
  • 3.4 Operational heap model
  • 3.5 Metatheory
  • 4 Implementation
  • 4.1 Frontend
  • 4.2 Compilation and Evaluation
  • 5 Related Work
  • 6 Future Work
  • 7 Conclusion
  • References
  • A Framework for Substructural Type Systems
  • 1 Introduction
  • 2 Vectors over semirings
  • 3 Bunched Typing Rules
  • 4 Generic syntax
  • 4.1 Descriptions of Systems
  • 4.2 Terms of a System
  • 4.3 Other syntaxes and syntactic forms
  • 5 Environments
  • 6 Semantics
  • 6.1 A layer of syntax is functorial
  • 6.2 The Kripke function space
  • 6.3 Semantic traversal
  • 7 Example traversals
  • 7.1 Renaming and substitution
  • 7.2 A usage elaborator
  • 7.3 A denotational semantics
  • 8 Conclusions
  • References
  • A Dependent Dependency Calculus
  • 1 Dependency Analysis
  • 2 Irrelevance and Dependent Types
  • 2.1 Run-time irrelevance
  • 2.2 Compile-time Irrelevance
  • 2.3 Strong Irrelevant Σ-types.
  • 3 A Simple Dependency Analyzing Calculus.

Similar Items