top

  Info

  • Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.

Biblioteca

MARC Lista (tabellare)
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 / / editor, Ilya Sergey
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 / / editor, Ilya Sergey
Autore Sergey Ilya
Pubbl/distr/stampa Cham, : Springer International Publishing AG, 2022
Descrizione fisica 1 online resource (xiv, 604 pages) : illustrations
Altri autori (Persone) SergeyIlya
Collana Lecture notes in computer science
Soggetto topico Computer programming
Programming languages (Electronic computers)
Soggetto non controllato automata theory
computer programming
computer systems
databases
distributed computer systems
distributed systems
embedded systems
formal languages
formal logic
linguistics
ontologies
parallel processing systems
program compilers
programming languages
semantics
software design
software engineering
software quality
verification
ISBN 3-030-99336-1
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Record Nr. UNISA-996464540903316
Sergey Ilya  
Cham, : Springer International Publishing AG, 2022
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
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 / / editor, Ilya Sergey
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 / / editor, Ilya Sergey
Autore Sergey Ilya
Edizione [1st ed.]
Pubbl/distr/stampa Cham, : Springer International Publishing AG, 2022
Descrizione fisica 1 online resource (xiv, 604 pages) : illustrations
Altri autori (Persone) SergeyIlya
Collana Lecture notes in computer science
Soggetto topico Computer programming
Programming languages (Electronic computers)
Programació (Ordinadors)
Llenguatges de programació
Soggetto genere / forma Congressos
Llibres electrònics
ISBN 9783030993368
3030993361
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto 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.
Record Nr. UNINA-9910555236003321
Sergey Ilya  
Cham, : Springer International Publishing AG, 2022
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui