|
|
|
|
| LEADER |
11201nam a22004573i 4500 |
| 001 |
EBC6941372 |
| 003 |
MiAaPQ |
| 005 |
20231204023222.0 |
| 006 |
m o d | |
| 007 |
cr cnu|||||||| |
| 008 |
231204s2022 xx o ||||0 eng d |
| 020 |
|
|
|a 9783030993368
|q (electronic bk.)
|
| 020 |
|
|
|z 9783030993351
|
| 035 |
|
|
|a (MiAaPQ)EBC6941372
|
| 035 |
|
|
|a (Au-PeEL)EBL6941372
|
| 035 |
|
|
|a (OCoLC)1308974291
|
| 040 |
|
|
|a MiAaPQ
|b eng
|e rda
|e pn
|c MiAaPQ
|d MiAaPQ
|
| 050 |
|
4 |
|a QA76.76.C65
|
| 100 |
1 |
|
|a Sergey, Ilya.
|
| 245 |
1 |
0 |
|a Programming Languages and Systems :
|b 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.
|
| 250 |
|
|
|a 1st ed.
|
| 264 |
|
1 |
|a Cham :
|b Springer International Publishing AG,
|c 2022.
|
| 264 |
|
4 |
|c ©2022.
|
| 300 |
|
|
|a 1 online resource (618 pages)
|
| 336 |
|
|
|a text
|b txt
|2 rdacontent
|
| 337 |
|
|
|a computer
|b c
|2 rdamedia
|
| 338 |
|
|
|a online resource
|b cr
|2 rdacarrier
|
| 490 |
1 |
|
|a Lecture Notes in Computer Science Series ;
|v v.13240
|
| 505 |
0 |
|
|a 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.
|
| 505 |
8 |
|
|a 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.
|
| 505 |
8 |
|
|a 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.
|
| 505 |
8 |
|
|a 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.
|
| 505 |
8 |
|
|a 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.
|
| 505 |
8 |
|
|a 3 A Simple Dependency Analyzing Calculus.
|
| 588 |
|
|
|a Description based on publisher supplied metadata and other sources.
|
| 590 |
|
|
|a Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2023. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries.
|
| 655 |
|
4 |
|a Electronic books.
|
| 776 |
0 |
8 |
|i Print version:
|a Sergey, Ilya
|t Programming Languages and Systems
|d Cham : Springer International Publishing AG,c2022
|z 9783030993351
|
| 797 |
2 |
|
|a ProQuest (Firm)
|
| 830 |
|
0 |
|a Lecture Notes in Computer Science Series
|
| 856 |
4 |
0 |
|u https://ebookcentral.proquest.com/lib/matrademy/detail.action?docID=6941372
|z Click to View
|
