Foundations of Software Science and Computation Structures : : 25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.13242 |
---|---|
: | |
TeilnehmendeR: | |
Place / Publishing House: | Cham : : Springer International Publishing AG,, 2022. ©2022. |
Year of Publication: | 2022 |
Edition: | 1st ed. |
Language: | English |
Series: | Lecture Notes in Computer Science Series
|
Online Access: | |
Physical Description: | 1 online resource (484 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
5006942704 |
---|---|
ctrlnum |
(MiAaPQ)5006942704 (Au-PeEL)EBL6942704 (OCoLC)1308973551 |
collection |
bib_alma |
record_format |
marc |
spelling |
Bouyer, Patricia. Foundations of Software Science and Computation Structures : 25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. 1st ed. Cham : Springer International Publishing AG, 2022. ©2022. 1 online resource (484 pages) text txt rdacontent computer c rdamedia online resource cr rdacarrier Lecture Notes in Computer Science Series ; v.13242 Intro -- ETAPS Foreword -- Preface -- Organization -- Parameterized Verification to the Rescue of Distributed Algorithms (Abstract of Invited Talk) -- Contents -- Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 NFAs, UFAs, DFAs, NBAs, UBAs, SUBAs, and DBAs -- 2.2 LTL formulas -- 2.3 M2MAs -- 2.4 Size lower bounds for DFAs, M2MAs and NFAs -- 3 M2MAs as representations of regular languages -- 3.1 M2MAs: procedures for operations and properties -- 3.2 Conciseness comparisons for regular languages -- 4 Representing regular omega-languages using regularlanguages -- 5 Conciseness comparisons for regular omega-languages -- 5.1 Size increases for LTL formulas -- 5.2 Size increases for DBAs, NBAs, SUBAs -- 6 Empirical results -- 6.1 SUBAs to minimized M2MAs and DFAs -- 6.2 NBAs and DBAs to minimized M2MAs -- 6.3 LTL formulas to minimized M2MAs -- 7 Summary and conclusions -- References -- Limits and difficulties in the design of under-approximation abstract domains -- 1 Introduction -- 2 Background -- 3 Integer Domains -- 3.1 Infinite Integer Domain -- 3.2 Finite Integer Domain -- 4 Arbitrary domains -- 4.1 Local Requirements for Impossibility -- 4.2 Global Requirements for Impossibility -- 5 On the necessity of high surjectivity hypothesis -- 6 Conclusions and Future Works -- References -- On probability-raising causality in Markov decision processes -- 1 Introduction -- 2 Preliminaries -- 3 Strict and global probability-raising causes -- 3.1 Examples and simple properties of probability-raising causes -- 3.2 Related work -- 4 Checking the existence of PR causes and the PR conditions -- 4.1 Checking the strict probability-raising condition and the existence of causes -- 4.2 Checking the global probability-raising condition -- 5 Quality and optimality of causes. 5.1 Quality measures for causes -- 5.2 Computation schemes for the quality measures for fixed cause set -- 5.3 Quality-optimal probability-raising causes -- 6 Conclusion -- References -- Parameterized Analysis of Reconfigurable Broadcast Networks -- 1 Introduction -- 2 Preliminaries -- 2.1 Multisets -- 2.2 Reconfigurable Broadcast Networks -- 2.3 Cubes and Counting Sets -- 3 Reachability sets of counting sets -- 3.1 Symbolic graph -- 3.2 Properties of the symbolic graph -- 4 The PSPACE Theorem -- 5 Application 1: Almost-sure coverability -- 5.1 The almost-sure coverability problem -- 5.2 A characterization of almost-sure coverability -- 5.3 PSPACE-completeness of the almost-sure coverability problem -- 6 Application 2: Computation by RBN -- 6.1 RBN Protocols -- 6.2 Expressivity -- References -- Separators in Continuous Petri Nets -- 1 Introduction -- 2 Preliminaries -- 2.1 Separators and bi-separators -- 3 A characterization of unreachability -- 4 Separators as certificates -- 4.1 Locally closed bi-separators -- 5 Constructing locally closed bi-separators -- 6 Checking locally closed bi-separators is in NC -- 7 Bi-separators for set-to-set unreachability -- 8 Conclusion -- References -- Graphical Piecewise-Linear Algebra -- 1 Introduction -- 2 Preliminaries -- 2.1 Props and Symmetric Monoidal Theories -- 2.2 Ordered Props and Symmetric Monoidal Inequality Theories -- 2.3 Graphical Polyhedral Algebra -- 3 Symmetric Monoidal Semi-Lattice Theories -- 4 The Theory of Piecewise-Linear Relations -- 4.1 Syntax and Semantics -- 4.2 Equational Theory -- 4.3 Completeness Theorem -- 5 Generating Piecewise-Linear Relations -- 5.1 The n-Fold Union Generators -- 5.2 The Simplest Non-Convex Diagram -- 5.3 The Semantics of a Diode -- 5.4 Alternative generators: max, ReLu and abs -- 5.5 Conclusion -- 6 Case Study: Electronic Circuits -- References. Token Games and History-Deterministic Quantitative Automata -- 1 Introduction -- 2 Preliminaries -- 3 Token Games -- 4 Deciding History-Determinism via One-Token Games -- 5 Deciding History-Determinism via Two Token Games -- 5.1 G₂ on LimSup and LimInf Automata -- 5.2 G₂ Characterises HDness for LimSup and LimInf Automata -- 6 Conclusions -- Acknowledgments -- References -- On the Translation of Automatato Linear Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 3 Unary Alphabet -- 4 General Alphabet -- 4.1 Cascaded Automata -- 4.2 Encoding Reachability within Reset Cascades by LTL Formulas -- 4.3 Depth and Length Analysis -- 4.4 Translating Deterministic Counter-Free Automata to LTL -- 5 Conclusions -- References -- Categorical composable cryptography -- 1 Introduction -- 1.1 Related work -- 2 Resource theories -- 3 Cryptography as a resource theory -- 4 Computational security -- 5 Applications -- 6 Outlook -- References -- DyNetKAT: An Algebra of Dynamic Networks -- 1 Introduction -- 2 Language Design -- 2.1 Brief Overview of NetKAT -- 2.2 Design Decisions -- 2.3 DyNetKAT Syntax -- 2.4 DyNetKAT Semantics -- 3 Semantic Results -- 4 A Framework for Safety -- 5 Implementation -- 6 Experimental Evaluation -- 7 Conclusions -- References -- A new criterion for M, N-adhesivity, with an application to hierarchical graphs -- 1 Introduction -- 2 M,N-adhesivity via creation of (co)limits -- 2.1 M, N-adhesive categories -- 2.2 A new criterion for M, N-adhesivity -- 2.3 Comma categories -- 3 Some paradigmatic examples -- 3.1 Directed (acyclic) graphs -- 3.2 Tree Orders -- 3.3 Various kinds of hierarchical graphs -- 4 Conclusions -- References -- Quantifier elimination for counting extensions of Presburger arithmetic -- 1 Introduction -- 2 Presburger arithmetic with counting quantifiers -- 3 A quantifier elimination procedure for PAC. 4 Discussion, summary of results and roadmap -- 5 The monadically-guarded fragment of PAC -- 6 Eliminating monadically-guarded counting quantifiers -- 7 The monadically-guarded fragment is in doubly exponential space -- 8 A complexity characterisation -- 9 Conclusion -- References -- A first-order logic characterisation of safety and co-safety languages -- 1 Introduction -- 2 Preliminaries -- 3 Safety-FO and coSafety-FO -- 4 Safety-FO captures LTL-definable safety languages -- 5 Conclusions -- References -- First-order separation over countable ordinals -- 1 Introduction -- 2 Preliminaries -- 2.1 Ordinals -- 2.2 Ordinal words -- 2.3 Ordinal monoids -- 2.4 First-order logic -- 3 The algorithm -- 3.1 The saturation construction -- 3.2 The algorithm -- 4 When the algorithm says 'no' -- 5 When the algorithm says 'yes' -- 5.1 Merge operators and FO-approximants -- 5.2 Construction of FO-approximants for words of finite andω-length -- 5.3 Construction of FO-approximants for countable ordinal words -- 6 Related problems -- 7 Conclusion -- References -- A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications -- 1 Introduction -- 2 A Calculus with Generalized Applications -- 2.1 Syntax and Semantics -- 2.2 Towards a Call-by-Name Operational Semantics -- 2.3 Some (Un)typed Properties of λJ -- 3 Inductive Characterization of Strong Normalization -- 3.1 ISN in the λ-Calculus Through Weak-Head Contexts -- 3.2 ISN for dβ -- 4 Quantitative Types Characterize Strong Normalization -- 4.1 The Typing System -- 4.2 The Characterization of dβ-Strong Normalization -- 4.3 Why π Is Not Quantitative -- 5 Faithfulness of the Translation -- 5.1 Explicit Substitutions -- 5.2 Proof of Faithfulness -- 6 Equivalent Notions of Strong Normalization -- 6.1 β-Normalization Is Not Enough -- 6.2 Comparison with β + p2 -- 6.3 Comparison with β + π. 6.4 Consequences for ΛJ -- 7 Conclusion -- References -- Modal Logics and Local Quantifiers:A Zoo in the Elementary Hierarchy -- 1 Introduction -- 2 Preliminaries -- 3 Lower bounds for ML(9kFO) and ML(9kSO) -- 4 Upper bounds via a small-model property for ML(9kSO) -- 5 Further connections -- References -- Temporal Stream Logic modulo Theories -- 1 Introduction -- 2 Preliminaries -- 3 Temporal Stream Logic modulo Theories -- 3.1 Temporal Stream Logic -- 3.2 Extending TSL with Theories -- 4 TSL modulo TU Satisfiability Checking -- 4.1 Buchi Stream Automata -- 4.2 An Algorithm for TSL modulo TU Satisfiability Checking -- 5 Undecidability of TSL modulo TU Satisfiability -- 6 (Semi-)Decidable Fragments -- 7 Evaluation -- 8 Related Work -- 9 Conclusion -- References -- The Different Shades of Infinite Session Types -- 1 Introduction -- 2 Shades of types -- 3 Types, trees and traces -- 4 From types to automata -- 5 From automata to types -- 6 Related work -- 7 Conclusion -- References -- Complete and tractable machine-independent characterizations of second-order polytime -- 1 Introduction -- 2 A second-order language with imperative procedures -- 3 Type system -- 4 Characterizations of the class of Basic Feasible Functionals -- 5 A completeness-preserving termination criterion -- 6 Conclusion and future work -- References -- Variable binding and substitution for (nameless) dummies -- 1 Introduction -- 2 De Bruijn monads -- 2.1 Definition of De Bruijn monads -- 2.2 Lifting assignments -- 2.3 Binding arities and binding conditions -- 2.4 Binding signatures and algebras -- 3 Initial-algebra semantics of binding signatures in De Bruijn monads -- 3.1 A category of De Bruijn monads -- 3.2 Categories of De Bruijn algebras -- 4 Relation to presheaf-based models -- 4.1 Trimming down presheaf-based models -- 4.2 Trimming down De Bruijn monads. 4.3 Bridging the gap. Description based on publisher supplied metadata and other sources. Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. Electronic books. Schröder, Lutz. Print version: Bouyer, Patricia Foundations of Software Science and Computation Structures Cham : Springer International Publishing AG,c2022 9783030992521 ProQuest (Firm) Lecture Notes in Computer Science Series https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6942704 Click to View |
language |
English |
format |
eBook |
author |
Bouyer, Patricia. |
spellingShingle |
Bouyer, Patricia. Foundations of Software Science and Computation Structures : 25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. Lecture Notes in Computer Science Series ; Intro -- ETAPS Foreword -- Preface -- Organization -- Parameterized Verification to the Rescue of Distributed Algorithms (Abstract of Invited Talk) -- Contents -- Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 NFAs, UFAs, DFAs, NBAs, UBAs, SUBAs, and DBAs -- 2.2 LTL formulas -- 2.3 M2MAs -- 2.4 Size lower bounds for DFAs, M2MAs and NFAs -- 3 M2MAs as representations of regular languages -- 3.1 M2MAs: procedures for operations and properties -- 3.2 Conciseness comparisons for regular languages -- 4 Representing regular omega-languages using regularlanguages -- 5 Conciseness comparisons for regular omega-languages -- 5.1 Size increases for LTL formulas -- 5.2 Size increases for DBAs, NBAs, SUBAs -- 6 Empirical results -- 6.1 SUBAs to minimized M2MAs and DFAs -- 6.2 NBAs and DBAs to minimized M2MAs -- 6.3 LTL formulas to minimized M2MAs -- 7 Summary and conclusions -- References -- Limits and difficulties in the design of under-approximation abstract domains -- 1 Introduction -- 2 Background -- 3 Integer Domains -- 3.1 Infinite Integer Domain -- 3.2 Finite Integer Domain -- 4 Arbitrary domains -- 4.1 Local Requirements for Impossibility -- 4.2 Global Requirements for Impossibility -- 5 On the necessity of high surjectivity hypothesis -- 6 Conclusions and Future Works -- References -- On probability-raising causality in Markov decision processes -- 1 Introduction -- 2 Preliminaries -- 3 Strict and global probability-raising causes -- 3.1 Examples and simple properties of probability-raising causes -- 3.2 Related work -- 4 Checking the existence of PR causes and the PR conditions -- 4.1 Checking the strict probability-raising condition and the existence of causes -- 4.2 Checking the global probability-raising condition -- 5 Quality and optimality of causes. 5.1 Quality measures for causes -- 5.2 Computation schemes for the quality measures for fixed cause set -- 5.3 Quality-optimal probability-raising causes -- 6 Conclusion -- References -- Parameterized Analysis of Reconfigurable Broadcast Networks -- 1 Introduction -- 2 Preliminaries -- 2.1 Multisets -- 2.2 Reconfigurable Broadcast Networks -- 2.3 Cubes and Counting Sets -- 3 Reachability sets of counting sets -- 3.1 Symbolic graph -- 3.2 Properties of the symbolic graph -- 4 The PSPACE Theorem -- 5 Application 1: Almost-sure coverability -- 5.1 The almost-sure coverability problem -- 5.2 A characterization of almost-sure coverability -- 5.3 PSPACE-completeness of the almost-sure coverability problem -- 6 Application 2: Computation by RBN -- 6.1 RBN Protocols -- 6.2 Expressivity -- References -- Separators in Continuous Petri Nets -- 1 Introduction -- 2 Preliminaries -- 2.1 Separators and bi-separators -- 3 A characterization of unreachability -- 4 Separators as certificates -- 4.1 Locally closed bi-separators -- 5 Constructing locally closed bi-separators -- 6 Checking locally closed bi-separators is in NC -- 7 Bi-separators for set-to-set unreachability -- 8 Conclusion -- References -- Graphical Piecewise-Linear Algebra -- 1 Introduction -- 2 Preliminaries -- 2.1 Props and Symmetric Monoidal Theories -- 2.2 Ordered Props and Symmetric Monoidal Inequality Theories -- 2.3 Graphical Polyhedral Algebra -- 3 Symmetric Monoidal Semi-Lattice Theories -- 4 The Theory of Piecewise-Linear Relations -- 4.1 Syntax and Semantics -- 4.2 Equational Theory -- 4.3 Completeness Theorem -- 5 Generating Piecewise-Linear Relations -- 5.1 The n-Fold Union Generators -- 5.2 The Simplest Non-Convex Diagram -- 5.3 The Semantics of a Diode -- 5.4 Alternative generators: max, ReLu and abs -- 5.5 Conclusion -- 6 Case Study: Electronic Circuits -- References. Token Games and History-Deterministic Quantitative Automata -- 1 Introduction -- 2 Preliminaries -- 3 Token Games -- 4 Deciding History-Determinism via One-Token Games -- 5 Deciding History-Determinism via Two Token Games -- 5.1 G₂ on LimSup and LimInf Automata -- 5.2 G₂ Characterises HDness for LimSup and LimInf Automata -- 6 Conclusions -- Acknowledgments -- References -- On the Translation of Automatato Linear Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 3 Unary Alphabet -- 4 General Alphabet -- 4.1 Cascaded Automata -- 4.2 Encoding Reachability within Reset Cascades by LTL Formulas -- 4.3 Depth and Length Analysis -- 4.4 Translating Deterministic Counter-Free Automata to LTL -- 5 Conclusions -- References -- Categorical composable cryptography -- 1 Introduction -- 1.1 Related work -- 2 Resource theories -- 3 Cryptography as a resource theory -- 4 Computational security -- 5 Applications -- 6 Outlook -- References -- DyNetKAT: An Algebra of Dynamic Networks -- 1 Introduction -- 2 Language Design -- 2.1 Brief Overview of NetKAT -- 2.2 Design Decisions -- 2.3 DyNetKAT Syntax -- 2.4 DyNetKAT Semantics -- 3 Semantic Results -- 4 A Framework for Safety -- 5 Implementation -- 6 Experimental Evaluation -- 7 Conclusions -- References -- A new criterion for M, N-adhesivity, with an application to hierarchical graphs -- 1 Introduction -- 2 M,N-adhesivity via creation of (co)limits -- 2.1 M, N-adhesive categories -- 2.2 A new criterion for M, N-adhesivity -- 2.3 Comma categories -- 3 Some paradigmatic examples -- 3.1 Directed (acyclic) graphs -- 3.2 Tree Orders -- 3.3 Various kinds of hierarchical graphs -- 4 Conclusions -- References -- Quantifier elimination for counting extensions of Presburger arithmetic -- 1 Introduction -- 2 Presburger arithmetic with counting quantifiers -- 3 A quantifier elimination procedure for PAC. 4 Discussion, summary of results and roadmap -- 5 The monadically-guarded fragment of PAC -- 6 Eliminating monadically-guarded counting quantifiers -- 7 The monadically-guarded fragment is in doubly exponential space -- 8 A complexity characterisation -- 9 Conclusion -- References -- A first-order logic characterisation of safety and co-safety languages -- 1 Introduction -- 2 Preliminaries -- 3 Safety-FO and coSafety-FO -- 4 Safety-FO captures LTL-definable safety languages -- 5 Conclusions -- References -- First-order separation over countable ordinals -- 1 Introduction -- 2 Preliminaries -- 2.1 Ordinals -- 2.2 Ordinal words -- 2.3 Ordinal monoids -- 2.4 First-order logic -- 3 The algorithm -- 3.1 The saturation construction -- 3.2 The algorithm -- 4 When the algorithm says 'no' -- 5 When the algorithm says 'yes' -- 5.1 Merge operators and FO-approximants -- 5.2 Construction of FO-approximants for words of finite andω-length -- 5.3 Construction of FO-approximants for countable ordinal words -- 6 Related problems -- 7 Conclusion -- References -- A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications -- 1 Introduction -- 2 A Calculus with Generalized Applications -- 2.1 Syntax and Semantics -- 2.2 Towards a Call-by-Name Operational Semantics -- 2.3 Some (Un)typed Properties of λJ -- 3 Inductive Characterization of Strong Normalization -- 3.1 ISN in the λ-Calculus Through Weak-Head Contexts -- 3.2 ISN for dβ -- 4 Quantitative Types Characterize Strong Normalization -- 4.1 The Typing System -- 4.2 The Characterization of dβ-Strong Normalization -- 4.3 Why π Is Not Quantitative -- 5 Faithfulness of the Translation -- 5.1 Explicit Substitutions -- 5.2 Proof of Faithfulness -- 6 Equivalent Notions of Strong Normalization -- 6.1 β-Normalization Is Not Enough -- 6.2 Comparison with β + p2 -- 6.3 Comparison with β + π. 6.4 Consequences for ΛJ -- 7 Conclusion -- References -- Modal Logics and Local Quantifiers:A Zoo in the Elementary Hierarchy -- 1 Introduction -- 2 Preliminaries -- 3 Lower bounds for ML(9kFO) and ML(9kSO) -- 4 Upper bounds via a small-model property for ML(9kSO) -- 5 Further connections -- References -- Temporal Stream Logic modulo Theories -- 1 Introduction -- 2 Preliminaries -- 3 Temporal Stream Logic modulo Theories -- 3.1 Temporal Stream Logic -- 3.2 Extending TSL with Theories -- 4 TSL modulo TU Satisfiability Checking -- 4.1 Buchi Stream Automata -- 4.2 An Algorithm for TSL modulo TU Satisfiability Checking -- 5 Undecidability of TSL modulo TU Satisfiability -- 6 (Semi-)Decidable Fragments -- 7 Evaluation -- 8 Related Work -- 9 Conclusion -- References -- The Different Shades of Infinite Session Types -- 1 Introduction -- 2 Shades of types -- 3 Types, trees and traces -- 4 From types to automata -- 5 From automata to types -- 6 Related work -- 7 Conclusion -- References -- Complete and tractable machine-independent characterizations of second-order polytime -- 1 Introduction -- 2 A second-order language with imperative procedures -- 3 Type system -- 4 Characterizations of the class of Basic Feasible Functionals -- 5 A completeness-preserving termination criterion -- 6 Conclusion and future work -- References -- Variable binding and substitution for (nameless) dummies -- 1 Introduction -- 2 De Bruijn monads -- 2.1 Definition of De Bruijn monads -- 2.2 Lifting assignments -- 2.3 Binding arities and binding conditions -- 2.4 Binding signatures and algebras -- 3 Initial-algebra semantics of binding signatures in De Bruijn monads -- 3.1 A category of De Bruijn monads -- 3.2 Categories of De Bruijn algebras -- 4 Relation to presheaf-based models -- 4.1 Trimming down presheaf-based models -- 4.2 Trimming down De Bruijn monads. 4.3 Bridging the gap. |
author_facet |
Bouyer, Patricia. Schröder, Lutz. |
author_variant |
p b pb |
author2 |
Schröder, Lutz. |
author2_variant |
l s ls |
author2_role |
TeilnehmendeR |
author_sort |
Bouyer, Patricia. |
title |
Foundations of Software Science and Computation Structures : 25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. |
title_sub |
25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. |
title_full |
Foundations of Software Science and Computation Structures : 25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. |
title_fullStr |
Foundations of Software Science and Computation Structures : 25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. |
title_full_unstemmed |
Foundations of Software Science and Computation Structures : 25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. |
title_auth |
Foundations of Software Science and Computation Structures : 25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. |
title_new |
Foundations of Software Science and Computation Structures : |
title_sort |
foundations of software science and computation structures : 25th international conference, fossacs 2022, held as part of the european joint conferences on theory and practice of software, etaps 2022, munich, germany, april 2-7, 2022, proceedings. |
series |
Lecture Notes in Computer Science Series ; |
series2 |
Lecture Notes in Computer Science Series ; |
publisher |
Springer International Publishing AG, |
publishDate |
2022 |
physical |
1 online resource (484 pages) |
edition |
1st ed. |
contents |
Intro -- ETAPS Foreword -- Preface -- Organization -- Parameterized Verification to the Rescue of Distributed Algorithms (Abstract of Invited Talk) -- Contents -- Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 NFAs, UFAs, DFAs, NBAs, UBAs, SUBAs, and DBAs -- 2.2 LTL formulas -- 2.3 M2MAs -- 2.4 Size lower bounds for DFAs, M2MAs and NFAs -- 3 M2MAs as representations of regular languages -- 3.1 M2MAs: procedures for operations and properties -- 3.2 Conciseness comparisons for regular languages -- 4 Representing regular omega-languages using regularlanguages -- 5 Conciseness comparisons for regular omega-languages -- 5.1 Size increases for LTL formulas -- 5.2 Size increases for DBAs, NBAs, SUBAs -- 6 Empirical results -- 6.1 SUBAs to minimized M2MAs and DFAs -- 6.2 NBAs and DBAs to minimized M2MAs -- 6.3 LTL formulas to minimized M2MAs -- 7 Summary and conclusions -- References -- Limits and difficulties in the design of under-approximation abstract domains -- 1 Introduction -- 2 Background -- 3 Integer Domains -- 3.1 Infinite Integer Domain -- 3.2 Finite Integer Domain -- 4 Arbitrary domains -- 4.1 Local Requirements for Impossibility -- 4.2 Global Requirements for Impossibility -- 5 On the necessity of high surjectivity hypothesis -- 6 Conclusions and Future Works -- References -- On probability-raising causality in Markov decision processes -- 1 Introduction -- 2 Preliminaries -- 3 Strict and global probability-raising causes -- 3.1 Examples and simple properties of probability-raising causes -- 3.2 Related work -- 4 Checking the existence of PR causes and the PR conditions -- 4.1 Checking the strict probability-raising condition and the existence of causes -- 4.2 Checking the global probability-raising condition -- 5 Quality and optimality of causes. 5.1 Quality measures for causes -- 5.2 Computation schemes for the quality measures for fixed cause set -- 5.3 Quality-optimal probability-raising causes -- 6 Conclusion -- References -- Parameterized Analysis of Reconfigurable Broadcast Networks -- 1 Introduction -- 2 Preliminaries -- 2.1 Multisets -- 2.2 Reconfigurable Broadcast Networks -- 2.3 Cubes and Counting Sets -- 3 Reachability sets of counting sets -- 3.1 Symbolic graph -- 3.2 Properties of the symbolic graph -- 4 The PSPACE Theorem -- 5 Application 1: Almost-sure coverability -- 5.1 The almost-sure coverability problem -- 5.2 A characterization of almost-sure coverability -- 5.3 PSPACE-completeness of the almost-sure coverability problem -- 6 Application 2: Computation by RBN -- 6.1 RBN Protocols -- 6.2 Expressivity -- References -- Separators in Continuous Petri Nets -- 1 Introduction -- 2 Preliminaries -- 2.1 Separators and bi-separators -- 3 A characterization of unreachability -- 4 Separators as certificates -- 4.1 Locally closed bi-separators -- 5 Constructing locally closed bi-separators -- 6 Checking locally closed bi-separators is in NC -- 7 Bi-separators for set-to-set unreachability -- 8 Conclusion -- References -- Graphical Piecewise-Linear Algebra -- 1 Introduction -- 2 Preliminaries -- 2.1 Props and Symmetric Monoidal Theories -- 2.2 Ordered Props and Symmetric Monoidal Inequality Theories -- 2.3 Graphical Polyhedral Algebra -- 3 Symmetric Monoidal Semi-Lattice Theories -- 4 The Theory of Piecewise-Linear Relations -- 4.1 Syntax and Semantics -- 4.2 Equational Theory -- 4.3 Completeness Theorem -- 5 Generating Piecewise-Linear Relations -- 5.1 The n-Fold Union Generators -- 5.2 The Simplest Non-Convex Diagram -- 5.3 The Semantics of a Diode -- 5.4 Alternative generators: max, ReLu and abs -- 5.5 Conclusion -- 6 Case Study: Electronic Circuits -- References. Token Games and History-Deterministic Quantitative Automata -- 1 Introduction -- 2 Preliminaries -- 3 Token Games -- 4 Deciding History-Determinism via One-Token Games -- 5 Deciding History-Determinism via Two Token Games -- 5.1 G₂ on LimSup and LimInf Automata -- 5.2 G₂ Characterises HDness for LimSup and LimInf Automata -- 6 Conclusions -- Acknowledgments -- References -- On the Translation of Automatato Linear Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 3 Unary Alphabet -- 4 General Alphabet -- 4.1 Cascaded Automata -- 4.2 Encoding Reachability within Reset Cascades by LTL Formulas -- 4.3 Depth and Length Analysis -- 4.4 Translating Deterministic Counter-Free Automata to LTL -- 5 Conclusions -- References -- Categorical composable cryptography -- 1 Introduction -- 1.1 Related work -- 2 Resource theories -- 3 Cryptography as a resource theory -- 4 Computational security -- 5 Applications -- 6 Outlook -- References -- DyNetKAT: An Algebra of Dynamic Networks -- 1 Introduction -- 2 Language Design -- 2.1 Brief Overview of NetKAT -- 2.2 Design Decisions -- 2.3 DyNetKAT Syntax -- 2.4 DyNetKAT Semantics -- 3 Semantic Results -- 4 A Framework for Safety -- 5 Implementation -- 6 Experimental Evaluation -- 7 Conclusions -- References -- A new criterion for M, N-adhesivity, with an application to hierarchical graphs -- 1 Introduction -- 2 M,N-adhesivity via creation of (co)limits -- 2.1 M, N-adhesive categories -- 2.2 A new criterion for M, N-adhesivity -- 2.3 Comma categories -- 3 Some paradigmatic examples -- 3.1 Directed (acyclic) graphs -- 3.2 Tree Orders -- 3.3 Various kinds of hierarchical graphs -- 4 Conclusions -- References -- Quantifier elimination for counting extensions of Presburger arithmetic -- 1 Introduction -- 2 Presburger arithmetic with counting quantifiers -- 3 A quantifier elimination procedure for PAC. 4 Discussion, summary of results and roadmap -- 5 The monadically-guarded fragment of PAC -- 6 Eliminating monadically-guarded counting quantifiers -- 7 The monadically-guarded fragment is in doubly exponential space -- 8 A complexity characterisation -- 9 Conclusion -- References -- A first-order logic characterisation of safety and co-safety languages -- 1 Introduction -- 2 Preliminaries -- 3 Safety-FO and coSafety-FO -- 4 Safety-FO captures LTL-definable safety languages -- 5 Conclusions -- References -- First-order separation over countable ordinals -- 1 Introduction -- 2 Preliminaries -- 2.1 Ordinals -- 2.2 Ordinal words -- 2.3 Ordinal monoids -- 2.4 First-order logic -- 3 The algorithm -- 3.1 The saturation construction -- 3.2 The algorithm -- 4 When the algorithm says 'no' -- 5 When the algorithm says 'yes' -- 5.1 Merge operators and FO-approximants -- 5.2 Construction of FO-approximants for words of finite andω-length -- 5.3 Construction of FO-approximants for countable ordinal words -- 6 Related problems -- 7 Conclusion -- References -- A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications -- 1 Introduction -- 2 A Calculus with Generalized Applications -- 2.1 Syntax and Semantics -- 2.2 Towards a Call-by-Name Operational Semantics -- 2.3 Some (Un)typed Properties of λJ -- 3 Inductive Characterization of Strong Normalization -- 3.1 ISN in the λ-Calculus Through Weak-Head Contexts -- 3.2 ISN for dβ -- 4 Quantitative Types Characterize Strong Normalization -- 4.1 The Typing System -- 4.2 The Characterization of dβ-Strong Normalization -- 4.3 Why π Is Not Quantitative -- 5 Faithfulness of the Translation -- 5.1 Explicit Substitutions -- 5.2 Proof of Faithfulness -- 6 Equivalent Notions of Strong Normalization -- 6.1 β-Normalization Is Not Enough -- 6.2 Comparison with β + p2 -- 6.3 Comparison with β + π. 6.4 Consequences for ΛJ -- 7 Conclusion -- References -- Modal Logics and Local Quantifiers:A Zoo in the Elementary Hierarchy -- 1 Introduction -- 2 Preliminaries -- 3 Lower bounds for ML(9kFO) and ML(9kSO) -- 4 Upper bounds via a small-model property for ML(9kSO) -- 5 Further connections -- References -- Temporal Stream Logic modulo Theories -- 1 Introduction -- 2 Preliminaries -- 3 Temporal Stream Logic modulo Theories -- 3.1 Temporal Stream Logic -- 3.2 Extending TSL with Theories -- 4 TSL modulo TU Satisfiability Checking -- 4.1 Buchi Stream Automata -- 4.2 An Algorithm for TSL modulo TU Satisfiability Checking -- 5 Undecidability of TSL modulo TU Satisfiability -- 6 (Semi-)Decidable Fragments -- 7 Evaluation -- 8 Related Work -- 9 Conclusion -- References -- The Different Shades of Infinite Session Types -- 1 Introduction -- 2 Shades of types -- 3 Types, trees and traces -- 4 From types to automata -- 5 From automata to types -- 6 Related work -- 7 Conclusion -- References -- Complete and tractable machine-independent characterizations of second-order polytime -- 1 Introduction -- 2 A second-order language with imperative procedures -- 3 Type system -- 4 Characterizations of the class of Basic Feasible Functionals -- 5 A completeness-preserving termination criterion -- 6 Conclusion and future work -- References -- Variable binding and substitution for (nameless) dummies -- 1 Introduction -- 2 De Bruijn monads -- 2.1 Definition of De Bruijn monads -- 2.2 Lifting assignments -- 2.3 Binding arities and binding conditions -- 2.4 Binding signatures and algebras -- 3 Initial-algebra semantics of binding signatures in De Bruijn monads -- 3.1 A category of De Bruijn monads -- 3.2 Categories of De Bruijn algebras -- 4 Relation to presheaf-based models -- 4.1 Trimming down presheaf-based models -- 4.2 Trimming down De Bruijn monads. 4.3 Bridging the gap. |
isbn |
9783030992538 9783030992521 |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA75 |
callnumber-sort |
QA 275.5 276.95 |
genre |
Electronic books. |
genre_facet |
Electronic books. |
url |
https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6942704 |
illustrated |
Not Illustrated |
oclc_num |
1308973551 |
work_keys_str_mv |
AT bouyerpatricia foundationsofsoftwarescienceandcomputationstructures25thinternationalconferencefossacs2022heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2022munichgermanyapril272022proceedings AT schroderlutz foundationsofsoftwarescienceandcomputationstructures25thinternationalconferencefossacs2022heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2022munichgermanyapril272022proceedings |
status_str |
n |
ids_txt_mv |
(MiAaPQ)5006942704 (Au-PeEL)EBL6942704 (OCoLC)1308973551 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Lecture Notes in Computer Science Series ; v.13242 |
is_hierarchy_title |
Foundations of Software Science and Computation Structures : 25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. |
container_title |
Lecture Notes in Computer Science Series ; v.13242 |
author2_original_writing_str_mv |
noLinkedField |
_version_ |
1792331062199713792 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>11355nam a22004693i 4500</leader><controlfield tag="001">5006942704</controlfield><controlfield tag="003">MiAaPQ</controlfield><controlfield tag="005">20240229073845.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr cnu||||||||</controlfield><controlfield tag="008">240229s2022 xx o ||||0 eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9783030992538</subfield><subfield code="q">(electronic bk.)</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="z">9783030992521</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)5006942704</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL6942704</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1308973551</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">MiAaPQ</subfield><subfield code="b">eng</subfield><subfield code="e">rda</subfield><subfield code="e">pn</subfield><subfield code="c">MiAaPQ</subfield><subfield code="d">MiAaPQ</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA75.5-76.95</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Bouyer, Patricia.</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Foundations of Software Science and Computation Structures :</subfield><subfield code="b">25th International Conference, FOSSACS 2022, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings.</subfield></datafield><datafield tag="250" ind1=" " ind2=" "><subfield code="a">1st ed.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Cham :</subfield><subfield code="b">Springer International Publishing AG,</subfield><subfield code="c">2022.</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2022.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (484 pages)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="490" ind1="1" ind2=" "><subfield code="a">Lecture Notes in Computer Science Series ;</subfield><subfield code="v">v.13242</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">Intro -- ETAPS Foreword -- Preface -- Organization -- Parameterized Verification to the Rescue of Distributed Algorithms (Abstract of Invited Talk) -- Contents -- Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 NFAs, UFAs, DFAs, NBAs, UBAs, SUBAs, and DBAs -- 2.2 LTL formulas -- 2.3 M2MAs -- 2.4 Size lower bounds for DFAs, M2MAs and NFAs -- 3 M2MAs as representations of regular languages -- 3.1 M2MAs: procedures for operations and properties -- 3.2 Conciseness comparisons for regular languages -- 4 Representing regular omega-languages using regularlanguages -- 5 Conciseness comparisons for regular omega-languages -- 5.1 Size increases for LTL formulas -- 5.2 Size increases for DBAs, NBAs, SUBAs -- 6 Empirical results -- 6.1 SUBAs to minimized M2MAs and DFAs -- 6.2 NBAs and DBAs to minimized M2MAs -- 6.3 LTL formulas to minimized M2MAs -- 7 Summary and conclusions -- References -- Limits and difficulties in the design of under-approximation abstract domains -- 1 Introduction -- 2 Background -- 3 Integer Domains -- 3.1 Infinite Integer Domain -- 3.2 Finite Integer Domain -- 4 Arbitrary domains -- 4.1 Local Requirements for Impossibility -- 4.2 Global Requirements for Impossibility -- 5 On the necessity of high surjectivity hypothesis -- 6 Conclusions and Future Works -- References -- On probability-raising causality in Markov decision processes -- 1 Introduction -- 2 Preliminaries -- 3 Strict and global probability-raising causes -- 3.1 Examples and simple properties of probability-raising causes -- 3.2 Related work -- 4 Checking the existence of PR causes and the PR conditions -- 4.1 Checking the strict probability-raising condition and the existence of causes -- 4.2 Checking the global probability-raising condition -- 5 Quality and optimality of causes.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">5.1 Quality measures for causes -- 5.2 Computation schemes for the quality measures for fixed cause set -- 5.3 Quality-optimal probability-raising causes -- 6 Conclusion -- References -- Parameterized Analysis of Reconfigurable Broadcast Networks -- 1 Introduction -- 2 Preliminaries -- 2.1 Multisets -- 2.2 Reconfigurable Broadcast Networks -- 2.3 Cubes and Counting Sets -- 3 Reachability sets of counting sets -- 3.1 Symbolic graph -- 3.2 Properties of the symbolic graph -- 4 The PSPACE Theorem -- 5 Application 1: Almost-sure coverability -- 5.1 The almost-sure coverability problem -- 5.2 A characterization of almost-sure coverability -- 5.3 PSPACE-completeness of the almost-sure coverability problem -- 6 Application 2: Computation by RBN -- 6.1 RBN Protocols -- 6.2 Expressivity -- References -- Separators in Continuous Petri Nets -- 1 Introduction -- 2 Preliminaries -- 2.1 Separators and bi-separators -- 3 A characterization of unreachability -- 4 Separators as certificates -- 4.1 Locally closed bi-separators -- 5 Constructing locally closed bi-separators -- 6 Checking locally closed bi-separators is in NC -- 7 Bi-separators for set-to-set unreachability -- 8 Conclusion -- References -- Graphical Piecewise-Linear Algebra -- 1 Introduction -- 2 Preliminaries -- 2.1 Props and Symmetric Monoidal Theories -- 2.2 Ordered Props and Symmetric Monoidal Inequality Theories -- 2.3 Graphical Polyhedral Algebra -- 3 Symmetric Monoidal Semi-Lattice Theories -- 4 The Theory of Piecewise-Linear Relations -- 4.1 Syntax and Semantics -- 4.2 Equational Theory -- 4.3 Completeness Theorem -- 5 Generating Piecewise-Linear Relations -- 5.1 The n-Fold Union Generators -- 5.2 The Simplest Non-Convex Diagram -- 5.3 The Semantics of a Diode -- 5.4 Alternative generators: max, ReLu and abs -- 5.5 Conclusion -- 6 Case Study: Electronic Circuits -- References.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">Token Games and History-Deterministic Quantitative Automata -- 1 Introduction -- 2 Preliminaries -- 3 Token Games -- 4 Deciding History-Determinism via One-Token Games -- 5 Deciding History-Determinism via Two Token Games -- 5.1 G₂ on LimSup and LimInf Automata -- 5.2 G₂ Characterises HDness for LimSup and LimInf Automata -- 6 Conclusions -- Acknowledgments -- References -- On the Translation of Automatato Linear Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 3 Unary Alphabet -- 4 General Alphabet -- 4.1 Cascaded Automata -- 4.2 Encoding Reachability within Reset Cascades by LTL Formulas -- 4.3 Depth and Length Analysis -- 4.4 Translating Deterministic Counter-Free Automata to LTL -- 5 Conclusions -- References -- Categorical composable cryptography -- 1 Introduction -- 1.1 Related work -- 2 Resource theories -- 3 Cryptography as a resource theory -- 4 Computational security -- 5 Applications -- 6 Outlook -- References -- DyNetKAT: An Algebra of Dynamic Networks -- 1 Introduction -- 2 Language Design -- 2.1 Brief Overview of NetKAT -- 2.2 Design Decisions -- 2.3 DyNetKAT Syntax -- 2.4 DyNetKAT Semantics -- 3 Semantic Results -- 4 A Framework for Safety -- 5 Implementation -- 6 Experimental Evaluation -- 7 Conclusions -- References -- A new criterion for M, N-adhesivity, with an application to hierarchical graphs -- 1 Introduction -- 2 M,N-adhesivity via creation of (co)limits -- 2.1 M, N-adhesive categories -- 2.2 A new criterion for M, N-adhesivity -- 2.3 Comma categories -- 3 Some paradigmatic examples -- 3.1 Directed (acyclic) graphs -- 3.2 Tree Orders -- 3.3 Various kinds of hierarchical graphs -- 4 Conclusions -- References -- Quantifier elimination for counting extensions of Presburger arithmetic -- 1 Introduction -- 2 Presburger arithmetic with counting quantifiers -- 3 A quantifier elimination procedure for PAC.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4 Discussion, summary of results and roadmap -- 5 The monadically-guarded fragment of PAC -- 6 Eliminating monadically-guarded counting quantifiers -- 7 The monadically-guarded fragment is in doubly exponential space -- 8 A complexity characterisation -- 9 Conclusion -- References -- A first-order logic characterisation of safety and co-safety languages -- 1 Introduction -- 2 Preliminaries -- 3 Safety-FO and coSafety-FO -- 4 Safety-FO captures LTL-definable safety languages -- 5 Conclusions -- References -- First-order separation over countable ordinals -- 1 Introduction -- 2 Preliminaries -- 2.1 Ordinals -- 2.2 Ordinal words -- 2.3 Ordinal monoids -- 2.4 First-order logic -- 3 The algorithm -- 3.1 The saturation construction -- 3.2 The algorithm -- 4 When the algorithm says 'no' -- 5 When the algorithm says 'yes' -- 5.1 Merge operators and FO-approximants -- 5.2 Construction of FO-approximants for words of finite andω-length -- 5.3 Construction of FO-approximants for countable ordinal words -- 6 Related problems -- 7 Conclusion -- References -- A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications -- 1 Introduction -- 2 A Calculus with Generalized Applications -- 2.1 Syntax and Semantics -- 2.2 Towards a Call-by-Name Operational Semantics -- 2.3 Some (Un)typed Properties of λJ -- 3 Inductive Characterization of Strong Normalization -- 3.1 ISN in the λ-Calculus Through Weak-Head Contexts -- 3.2 ISN for dβ -- 4 Quantitative Types Characterize Strong Normalization -- 4.1 The Typing System -- 4.2 The Characterization of dβ-Strong Normalization -- 4.3 Why π Is Not Quantitative -- 5 Faithfulness of the Translation -- 5.1 Explicit Substitutions -- 5.2 Proof of Faithfulness -- 6 Equivalent Notions of Strong Normalization -- 6.1 β-Normalization Is Not Enough -- 6.2 Comparison with β + p2 -- 6.3 Comparison with β + π.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">6.4 Consequences for ΛJ -- 7 Conclusion -- References -- Modal Logics and Local Quantifiers:A Zoo in the Elementary Hierarchy -- 1 Introduction -- 2 Preliminaries -- 3 Lower bounds for ML(9kFO) and ML(9kSO) -- 4 Upper bounds via a small-model property for ML(9kSO) -- 5 Further connections -- References -- Temporal Stream Logic modulo Theories -- 1 Introduction -- 2 Preliminaries -- 3 Temporal Stream Logic modulo Theories -- 3.1 Temporal Stream Logic -- 3.2 Extending TSL with Theories -- 4 TSL modulo TU Satisfiability Checking -- 4.1 Buchi Stream Automata -- 4.2 An Algorithm for TSL modulo TU Satisfiability Checking -- 5 Undecidability of TSL modulo TU Satisfiability -- 6 (Semi-)Decidable Fragments -- 7 Evaluation -- 8 Related Work -- 9 Conclusion -- References -- The Different Shades of Infinite Session Types -- 1 Introduction -- 2 Shades of types -- 3 Types, trees and traces -- 4 From types to automata -- 5 From automata to types -- 6 Related work -- 7 Conclusion -- References -- Complete and tractable machine-independent characterizations of second-order polytime -- 1 Introduction -- 2 A second-order language with imperative procedures -- 3 Type system -- 4 Characterizations of the class of Basic Feasible Functionals -- 5 A completeness-preserving termination criterion -- 6 Conclusion and future work -- References -- Variable binding and substitution for (nameless) dummies -- 1 Introduction -- 2 De Bruijn monads -- 2.1 Definition of De Bruijn monads -- 2.2 Lifting assignments -- 2.3 Binding arities and binding conditions -- 2.4 Binding signatures and algebras -- 3 Initial-algebra semantics of binding signatures in De Bruijn monads -- 3.1 A category of De Bruijn monads -- 3.2 Categories of De Bruijn algebras -- 4 Relation to presheaf-based models -- 4.1 Trimming down presheaf-based models -- 4.2 Trimming down De Bruijn monads.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4.3 Bridging the gap.</subfield></datafield><datafield tag="588" ind1=" " ind2=" "><subfield code="a">Description based on publisher supplied metadata and other sources.</subfield></datafield><datafield tag="590" ind1=" " ind2=" "><subfield code="a">Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. </subfield></datafield><datafield tag="655" ind1=" " ind2="4"><subfield code="a">Electronic books.</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Schröder, Lutz.</subfield></datafield><datafield tag="776" ind1="0" ind2="8"><subfield code="i">Print version:</subfield><subfield code="a">Bouyer, Patricia</subfield><subfield code="t">Foundations of Software Science and Computation Structures</subfield><subfield code="d">Cham : Springer International Publishing AG,c2022</subfield><subfield code="z">9783030992521</subfield></datafield><datafield tag="797" ind1="2" ind2=" "><subfield code="a">ProQuest (Firm)</subfield></datafield><datafield tag="830" ind1=" " ind2="0"><subfield code="a">Lecture Notes in Computer Science Series</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6942704</subfield><subfield code="z">Click to View</subfield></datafield></record></collection> |