.

0 (hodnocen0 x )

EB

ONLINE

Cham : Springer International Publishing AG, 2022

1 online resource (618 pages)

ISBN 9783030993368 (electronic bk.)

ISBN 9783030993351

Lecture Notes in Computer Science Ser. ; v.13240

Print version: Sergey, Ilya Programming Languages and Systems Cham : Springer International Publishing AG,c2022 ISBN 9783030993351

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 A Simple Dependency Analyzing Calculus.

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.

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.

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.

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 V-types.

001896860

express

(Au-PeEL)EBL6941372

(MiAaPQ)EBC6941372

(OCoLC)1308974291