Foundations of Software Science and Computation Structures : : 24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.12650 |
---|---|
: | |
TeilnehmendeR: | |
Place / Publishing House: | Cham : : Springer International Publishing AG,, 2021. ©2021. |
Year of Publication: | 2021 |
Edition: | 1st ed. |
Language: | English |
Series: | Lecture Notes in Computer Science Series
|
Online Access: | |
Physical Description: | 1 online resource (587 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
5006524970 |
---|---|
ctrlnum |
(MiAaPQ)5006524970 (Au-PeEL)EBL6524970 (OCoLC)1244535767 |
collection |
bib_alma |
record_format |
marc |
spelling |
Kiefer, Stefan. Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. 1st ed. Cham : Springer International Publishing AG, 2021. ©2021. 1 online resource (587 pages) text txt rdacontent computer c rdamedia online resource cr rdacarrier Lecture Notes in Computer Science Series ; v.12650 Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- Constructing a universe for the setoid model -- 1 Introduction -- 1.1 Related work -- 2 MLTT^Prop -- 2.1 Formalization -- 3 Setoid model -- 3.1 Setoid model as a CwF -- 3.2 Setoid Type Theory -- 4 Universe of setoids -- 4.1 Inductive-recursive universes -- 4.2 Inductive-recursive setoid universe -- 4.3 Inductive-inductive setoid universe -- 4.4 Inductive setoid universe -- 5 Conclusions and further work -- References -- Nominal Equational Problems -- 1 Introduction -- 2 Background -- 3 Nominal Equational Problems -- 4 A rule-based procedure -- 4.1 Simplification Rules -- 4.2 Soundness and Preservation of Solutions -- 4.3 Termination -- 5 Nominal Equational Solved Forms -- 6 Conclusion -- References -- Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy -- 1 Introduction -- 2 Preliminaries -- 3 The cut-off problem for acyclic Petri nets -- 3.1 Characterizing acyclic systems with cut-offs -- 3.2 Polynomial time algorithm -- 4 The Scaling and Insertion lemmas -- 4.1 The Scaling Lemma -- 4.2 The Insertion Lemma -- 5 Polynomial time algorithm for the general case -- 5.1 Characterizing systems with cut-offs -- 5.2 Polynomial time algorithm -- 6 Symmetric rendez-vous protocols -- 7 Symmetric protocols with leaders -- 7.1 A non-deterministic polynomial time algorithm -- References -- Fixpoint Theory - Upside Down -- 1 Introduction -- 2 Lattices and MV-Algebras -- 3 Non-expansive Functions and Their Approximations -- 4 Proof Rules -- 5 (De)Composing Functions and Approximations -- 6 Applications -- 6.1 Termination Probability -- 6.2 Behavioural Metrics for Probabilistic Automata -- 6.3 Bisimilarity -- 7 Simple Stochastic Games -- 8 Conclusion -- References -- Most of'' leads to undecidability: Failure of adding frequencies to LTL -- 1 Introduction -- 1.1 Related work. 2 Preliminaries -- 3 Playing with Half Operator -- 4 Undecidability of LTL extensions -- 4.1 "Half of" meets the halting problem -- Fact 5 -- Fact 6 -- 6.1 Undecidability of model-checking -- 6.2 Most-Frequent Letter and Undecidability -- 6.3 Most-Frequent Letter: the reduction -- 7 Decidable variants -- 8 Two-Variable First-Order Logic with Majority -- 9 Conclusions -- References -- Combining Semilattices and Semimodules -- 1 Introduction -- 2 (Weak) Distributive laws -- 3 The Powerset and Semimodule Monads -- 4 The Weak Distributive Law δ : SP → PS -- 5 The Weak Lifting of P to EM(S) -- 5.1 Proof of Theorem 24 -- 6 The Composite Monad: an Algebraic Presentation -- 7 Conclusions: Related and Future Work -- References -- One-way Resynchronizability of Word Transducers -- 1 Introduction -- 2 Preliminaries -- 3 One-way resynchronizability -- 3.1 Regular resynchronizers -- 3.2 Main result -- 4 Proof overview for Theorem 1 -- 4.1 Flows and inversions -- 4.2 Dominant output intervals -- 5 Proof of Theorem 1 -- 6 Proof overview of Theorem 2 -- 7 Complexity -- 8 Conclusions -- References -- Fair Refinement for Asynchronous Session Types -- 1 Introduction -- 2 Refinement for Asynchronous Session Types -- 2.1 Preliminaries: Asynchronous Session Types -- 2.2 Fair Refinement for Asynchronous Session Types -- 2.3 Controllability for Asynchronous Session Types -- 3 Fair Asynchronous Session Subtyping -- 4 A Sound Algorithm for Fair Asynchronous Subtyping -- 5 Implementation -- 6 Related and Future Work -- References -- Running Time Analysis of Broadcast Consensus Protocols -- 1 Introduction -- 2 Preliminaries -- 3 Example: Majority -- 4 Comparison with other Models -- 4.1 Non-Deterministic Broadcast Protocols -- 4.2 Population Protocols -- 5 Protocols for Presburger Arithmetic -- 5.1 Linear Inequalities -- 5.2 Modulo Predicates and Boolean Combinations. 6 Protocols for all Predicates in ZPL -- References -- Leafy automata for higher-order concurrency -- 1 Introduction -- 2 Finitary Idealized Concurrent Algol (FICA) -- 3 Game semantics -- 4 Leafy automata -- 5 Local leafy automata (LLA) -- 6 From FICA to LA -- 7 Local FICA -- 8 From LA to FICA -- 9 Conclusion and further work -- References -- Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic -- 1 Introduction -- 2 Background in Abstract Rewriting -- 3 λ-calculi: CbN, CbV, and bang -- 3.1 Call-by-Name and Call-by-Value λ-calculi -- 3.2 Bang calculi -- 3.3 CbN and CbV translations into the bang calculus -- 4 The least-level strategy -- 4.1 Least-level reduction in bang calculi -- 4.2 Least-level for a bang calculus: examples. -- 4.3 Least-level for CbN and CbV λ-calculi -- 5 Embedding of CbN and CbV by level -- 6 Least-level factorization via bang calculus -- 6.1 Factorization of →β! in a bang calculus -- 6.2 Pure calculi and least-level normalization -- 6.3 Least-level Factorization, Modularly -- 7 Case study: non-deterministic λ-calculi -- 8 Conclusions and Related Work -- References -- Generalized Bounded Linear Logic and its Categorical Semantics -- 1 Introduction -- 2 Generalized Bounded Linear Logic -- 2.1 Indexing 2-Category -- 2.2 Formulas and Proofs -- 2.3 Complexity of Cut-Elimination in GBLL -- 3 Translation from Constrained BLL -- 3.1 Resource Polynomials and Constraints -- 3.2 Formulas and Inference Rules of CBLL -- 3.3 Translation into GBAL+ -- 4 Categorical Semantics for GBLL -- 4.1 Semantics of GBLL -- 4.2 Construction of an Indexed Linear Exponential Comonad -- 4.3 GBLL Semantics by Realizability Category -- 5 Conclusion and Related Work -- References -- Focused Proof-search in the Logic of Bunched Implications -- 1 Introduction -- 2 Re-presentations of BI -- 2.1 Traditional Syntax -- 2.2 Sequent Calculus. 2.3 Nested Calculus -- 3 A Focused System -- 3.1 Polarisation -- 3.2 Focused Calculus -- 3.3 Completeness of fBI -- 4 Conclusion -- References -- Interpolation and Amalgamation for Arrays with MaxDiff -- 1 Introduction -- 2 Formal Preliminaries -- 3 Arrays with MaxDiff -- 3.1 Our roadmap -- 4 Embeddings -- 5 Amalgamation -- 6 Satisfiability -- 7 An interpolation algorithm -- 8 When indexes are just a total order -- 9 Conclusions and further work -- References -- Adjoint Reactive GUI Programming -- Introduction -- The Language -- Formal Calculus -- Semantics -- Related and Future Work -- References -- On the Expressiveness of Büchi Arithmetic -- 1 Introduction -- 2 Preliminaries -- 3 The inexpressiveness of existential Büchi arithmetic -- 4 Expressive completeness of the ∑2-fragment of Büchi arithmetic -- 5 Existential Büchi arithmetic defines regular languages of polynomial growth -- 6 Conclusion -- References -- Parametricity for Primitive Nested Types -- 1 Introduction -- 2 The Calculus -- 2.1 Types -- 2.2 Terms -- 3 Interpreting Types -- 3.1 Interpreting Types as Sets -- 3.2 Interpreting Types as Relations -- 4 The Identity Extension Lemma -- 5 Interpreting Terms -- 6 Free Theorems for Nested Types -- 6.1 Consequences of Naturality -- 6.2 The Abstraction Theorem -- 7 Conclusion and Directions for Future Work -- References -- The Spirit of Node Replication -- 1 Introduction -- 2 A Calculus for Node Replication -- 3 Operational Properties -- 4 Encoding Evaluation Strategies -- 4.1 Call-by-name -- 4.2 Call-by-need -- 5 A Type System for the λR-calculus -- 6 Observational Equivalence -- 7 Related Works and Conclusion -- References -- Nondeterministic and co-Nondeterministic Implies Deterministic, for Data Languages -- 1 Introduction -- 2 Data languages and register automata -- 3 Examples -- 4 Main results -- 5 Orbit-finite automata. 6 Proof of Theorem 1 -- 6.1 Examples -- 6.2 Proof of Lemma 1 -- 7 Application to Unambiguous Register Automata -- 8 Proof of Theorem 2 -- 9 Final remarks -- References -- Certifying Inexpressibility -- 1 Introduction -- 2 Preliminaries -- 2.1 Transducers and Realizability -- 2.2 Automata -- 3 Refuting DBW-Recognizability -- 3.1 Complexity -- 3.2 Certifying DBW-Refutation -- 4 Separability and Approximations -- 4.1 Refuting Separability -- 4.2 Certificate-Guided Approximation -- 5 Other Classes of Deterministic Automata -- 6 Discussion and Directions for Future Research -- References -- A General Semantic Construction of Dependent Refinement Type Systems, Categorically -- 1 Introduction -- 2 Preliminaries -- 3 Lifting SCCompCs and Fibred Coproducts -- 3.1 Lifting SCCompCs -- 3.2 Lifting Fibred Coproducts -- 4 Lifting Monads on SCCompCs -- 5 Soundness -- 5.1 Underlying Type System -- 5.2 Predicate Logic -- 5.3 Refinement Type System -- 5.4 Semantics -- 6 Toward Recursion in Refinement Type Systems -- 6.1 Conway Operators -- 6.2 Recursion in the Underlying Type System -- 7 Related Work -- 8 Conclusion and Future Work -- References -- Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP -- 1 Introduction -- 2 Preliminaries -- 3 Characterizing Energy-Parity via Gain and Bailout -- 4 Bailout -- 5 Gain -- 6 The Main Results -- 7 Conclusion and Outlook -- References -- Nondeterministic Syntactic Complexity -- 1 Introduction -- 2 Preliminaries -- 3 Duality Theory of Semilattice Automata -- 4 Boolean Representations and Subatomic NFAs -- 5 Applications -- 5.1 Unary languages -- 5.2 Languages with a canonical state-minimal nfa -- 6 Conclusion and Future Work -- References -- A String Diagrammatic Axiomatisation of Finite-State Automata -- 1 Introduction -- 2 Syntax and semantics -- 3 Equational theory. 4 Encoding regular expressions and automata. 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. Tasson, Christine. Print version: Kiefer, Stefan Foundations of Software Science and Computation Structures Cham : Springer International Publishing AG,c2021 9783030719944 ProQuest (Firm) Lecture Notes in Computer Science Series https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6524970 Click to View |
language |
English |
format |
eBook |
author |
Kiefer, Stefan. |
spellingShingle |
Kiefer, Stefan. Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. Lecture Notes in Computer Science Series ; Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- Constructing a universe for the setoid model -- 1 Introduction -- 1.1 Related work -- 2 MLTT^Prop -- 2.1 Formalization -- 3 Setoid model -- 3.1 Setoid model as a CwF -- 3.2 Setoid Type Theory -- 4 Universe of setoids -- 4.1 Inductive-recursive universes -- 4.2 Inductive-recursive setoid universe -- 4.3 Inductive-inductive setoid universe -- 4.4 Inductive setoid universe -- 5 Conclusions and further work -- References -- Nominal Equational Problems -- 1 Introduction -- 2 Background -- 3 Nominal Equational Problems -- 4 A rule-based procedure -- 4.1 Simplification Rules -- 4.2 Soundness and Preservation of Solutions -- 4.3 Termination -- 5 Nominal Equational Solved Forms -- 6 Conclusion -- References -- Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy -- 1 Introduction -- 2 Preliminaries -- 3 The cut-off problem for acyclic Petri nets -- 3.1 Characterizing acyclic systems with cut-offs -- 3.2 Polynomial time algorithm -- 4 The Scaling and Insertion lemmas -- 4.1 The Scaling Lemma -- 4.2 The Insertion Lemma -- 5 Polynomial time algorithm for the general case -- 5.1 Characterizing systems with cut-offs -- 5.2 Polynomial time algorithm -- 6 Symmetric rendez-vous protocols -- 7 Symmetric protocols with leaders -- 7.1 A non-deterministic polynomial time algorithm -- References -- Fixpoint Theory - Upside Down -- 1 Introduction -- 2 Lattices and MV-Algebras -- 3 Non-expansive Functions and Their Approximations -- 4 Proof Rules -- 5 (De)Composing Functions and Approximations -- 6 Applications -- 6.1 Termination Probability -- 6.2 Behavioural Metrics for Probabilistic Automata -- 6.3 Bisimilarity -- 7 Simple Stochastic Games -- 8 Conclusion -- References -- Most of'' leads to undecidability: Failure of adding frequencies to LTL -- 1 Introduction -- 1.1 Related work. 2 Preliminaries -- 3 Playing with Half Operator -- 4 Undecidability of LTL extensions -- 4.1 "Half of" meets the halting problem -- Fact 5 -- Fact 6 -- 6.1 Undecidability of model-checking -- 6.2 Most-Frequent Letter and Undecidability -- 6.3 Most-Frequent Letter: the reduction -- 7 Decidable variants -- 8 Two-Variable First-Order Logic with Majority -- 9 Conclusions -- References -- Combining Semilattices and Semimodules -- 1 Introduction -- 2 (Weak) Distributive laws -- 3 The Powerset and Semimodule Monads -- 4 The Weak Distributive Law δ : SP → PS -- 5 The Weak Lifting of P to EM(S) -- 5.1 Proof of Theorem 24 -- 6 The Composite Monad: an Algebraic Presentation -- 7 Conclusions: Related and Future Work -- References -- One-way Resynchronizability of Word Transducers -- 1 Introduction -- 2 Preliminaries -- 3 One-way resynchronizability -- 3.1 Regular resynchronizers -- 3.2 Main result -- 4 Proof overview for Theorem 1 -- 4.1 Flows and inversions -- 4.2 Dominant output intervals -- 5 Proof of Theorem 1 -- 6 Proof overview of Theorem 2 -- 7 Complexity -- 8 Conclusions -- References -- Fair Refinement for Asynchronous Session Types -- 1 Introduction -- 2 Refinement for Asynchronous Session Types -- 2.1 Preliminaries: Asynchronous Session Types -- 2.2 Fair Refinement for Asynchronous Session Types -- 2.3 Controllability for Asynchronous Session Types -- 3 Fair Asynchronous Session Subtyping -- 4 A Sound Algorithm for Fair Asynchronous Subtyping -- 5 Implementation -- 6 Related and Future Work -- References -- Running Time Analysis of Broadcast Consensus Protocols -- 1 Introduction -- 2 Preliminaries -- 3 Example: Majority -- 4 Comparison with other Models -- 4.1 Non-Deterministic Broadcast Protocols -- 4.2 Population Protocols -- 5 Protocols for Presburger Arithmetic -- 5.1 Linear Inequalities -- 5.2 Modulo Predicates and Boolean Combinations. 6 Protocols for all Predicates in ZPL -- References -- Leafy automata for higher-order concurrency -- 1 Introduction -- 2 Finitary Idealized Concurrent Algol (FICA) -- 3 Game semantics -- 4 Leafy automata -- 5 Local leafy automata (LLA) -- 6 From FICA to LA -- 7 Local FICA -- 8 From LA to FICA -- 9 Conclusion and further work -- References -- Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic -- 1 Introduction -- 2 Background in Abstract Rewriting -- 3 λ-calculi: CbN, CbV, and bang -- 3.1 Call-by-Name and Call-by-Value λ-calculi -- 3.2 Bang calculi -- 3.3 CbN and CbV translations into the bang calculus -- 4 The least-level strategy -- 4.1 Least-level reduction in bang calculi -- 4.2 Least-level for a bang calculus: examples. -- 4.3 Least-level for CbN and CbV λ-calculi -- 5 Embedding of CbN and CbV by level -- 6 Least-level factorization via bang calculus -- 6.1 Factorization of →β! in a bang calculus -- 6.2 Pure calculi and least-level normalization -- 6.3 Least-level Factorization, Modularly -- 7 Case study: non-deterministic λ-calculi -- 8 Conclusions and Related Work -- References -- Generalized Bounded Linear Logic and its Categorical Semantics -- 1 Introduction -- 2 Generalized Bounded Linear Logic -- 2.1 Indexing 2-Category -- 2.2 Formulas and Proofs -- 2.3 Complexity of Cut-Elimination in GBLL -- 3 Translation from Constrained BLL -- 3.1 Resource Polynomials and Constraints -- 3.2 Formulas and Inference Rules of CBLL -- 3.3 Translation into GBAL+ -- 4 Categorical Semantics for GBLL -- 4.1 Semantics of GBLL -- 4.2 Construction of an Indexed Linear Exponential Comonad -- 4.3 GBLL Semantics by Realizability Category -- 5 Conclusion and Related Work -- References -- Focused Proof-search in the Logic of Bunched Implications -- 1 Introduction -- 2 Re-presentations of BI -- 2.1 Traditional Syntax -- 2.2 Sequent Calculus. 2.3 Nested Calculus -- 3 A Focused System -- 3.1 Polarisation -- 3.2 Focused Calculus -- 3.3 Completeness of fBI -- 4 Conclusion -- References -- Interpolation and Amalgamation for Arrays with MaxDiff -- 1 Introduction -- 2 Formal Preliminaries -- 3 Arrays with MaxDiff -- 3.1 Our roadmap -- 4 Embeddings -- 5 Amalgamation -- 6 Satisfiability -- 7 An interpolation algorithm -- 8 When indexes are just a total order -- 9 Conclusions and further work -- References -- Adjoint Reactive GUI Programming -- Introduction -- The Language -- Formal Calculus -- Semantics -- Related and Future Work -- References -- On the Expressiveness of Büchi Arithmetic -- 1 Introduction -- 2 Preliminaries -- 3 The inexpressiveness of existential Büchi arithmetic -- 4 Expressive completeness of the ∑2-fragment of Büchi arithmetic -- 5 Existential Büchi arithmetic defines regular languages of polynomial growth -- 6 Conclusion -- References -- Parametricity for Primitive Nested Types -- 1 Introduction -- 2 The Calculus -- 2.1 Types -- 2.2 Terms -- 3 Interpreting Types -- 3.1 Interpreting Types as Sets -- 3.2 Interpreting Types as Relations -- 4 The Identity Extension Lemma -- 5 Interpreting Terms -- 6 Free Theorems for Nested Types -- 6.1 Consequences of Naturality -- 6.2 The Abstraction Theorem -- 7 Conclusion and Directions for Future Work -- References -- The Spirit of Node Replication -- 1 Introduction -- 2 A Calculus for Node Replication -- 3 Operational Properties -- 4 Encoding Evaluation Strategies -- 4.1 Call-by-name -- 4.2 Call-by-need -- 5 A Type System for the λR-calculus -- 6 Observational Equivalence -- 7 Related Works and Conclusion -- References -- Nondeterministic and co-Nondeterministic Implies Deterministic, for Data Languages -- 1 Introduction -- 2 Data languages and register automata -- 3 Examples -- 4 Main results -- 5 Orbit-finite automata. 6 Proof of Theorem 1 -- 6.1 Examples -- 6.2 Proof of Lemma 1 -- 7 Application to Unambiguous Register Automata -- 8 Proof of Theorem 2 -- 9 Final remarks -- References -- Certifying Inexpressibility -- 1 Introduction -- 2 Preliminaries -- 2.1 Transducers and Realizability -- 2.2 Automata -- 3 Refuting DBW-Recognizability -- 3.1 Complexity -- 3.2 Certifying DBW-Refutation -- 4 Separability and Approximations -- 4.1 Refuting Separability -- 4.2 Certificate-Guided Approximation -- 5 Other Classes of Deterministic Automata -- 6 Discussion and Directions for Future Research -- References -- A General Semantic Construction of Dependent Refinement Type Systems, Categorically -- 1 Introduction -- 2 Preliminaries -- 3 Lifting SCCompCs and Fibred Coproducts -- 3.1 Lifting SCCompCs -- 3.2 Lifting Fibred Coproducts -- 4 Lifting Monads on SCCompCs -- 5 Soundness -- 5.1 Underlying Type System -- 5.2 Predicate Logic -- 5.3 Refinement Type System -- 5.4 Semantics -- 6 Toward Recursion in Refinement Type Systems -- 6.1 Conway Operators -- 6.2 Recursion in the Underlying Type System -- 7 Related Work -- 8 Conclusion and Future Work -- References -- Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP -- 1 Introduction -- 2 Preliminaries -- 3 Characterizing Energy-Parity via Gain and Bailout -- 4 Bailout -- 5 Gain -- 6 The Main Results -- 7 Conclusion and Outlook -- References -- Nondeterministic Syntactic Complexity -- 1 Introduction -- 2 Preliminaries -- 3 Duality Theory of Semilattice Automata -- 4 Boolean Representations and Subatomic NFAs -- 5 Applications -- 5.1 Unary languages -- 5.2 Languages with a canonical state-minimal nfa -- 6 Conclusion and Future Work -- References -- A String Diagrammatic Axiomatisation of Finite-State Automata -- 1 Introduction -- 2 Syntax and semantics -- 3 Equational theory. 4 Encoding regular expressions and automata. |
author_facet |
Kiefer, Stefan. Tasson, Christine. |
author_variant |
s k sk |
author2 |
Tasson, Christine. |
author2_variant |
c t ct |
author2_role |
TeilnehmendeR |
author_sort |
Kiefer, Stefan. |
title |
Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. |
title_sub |
24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. |
title_full |
Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. |
title_fullStr |
Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. |
title_full_unstemmed |
Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. |
title_auth |
Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. |
title_new |
Foundations of Software Science and Computation Structures : |
title_sort |
foundations of software science and computation structures : 24th international conference, fossacs 2021, held as part of the european joint conferences on theory and practice of software, etaps 2021, luxembourg city, luxembourg, march 27 - april 1, 2021, proceedings. |
series |
Lecture Notes in Computer Science Series ; |
series2 |
Lecture Notes in Computer Science Series ; |
publisher |
Springer International Publishing AG, |
publishDate |
2021 |
physical |
1 online resource (587 pages) |
edition |
1st ed. |
contents |
Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- Constructing a universe for the setoid model -- 1 Introduction -- 1.1 Related work -- 2 MLTT^Prop -- 2.1 Formalization -- 3 Setoid model -- 3.1 Setoid model as a CwF -- 3.2 Setoid Type Theory -- 4 Universe of setoids -- 4.1 Inductive-recursive universes -- 4.2 Inductive-recursive setoid universe -- 4.3 Inductive-inductive setoid universe -- 4.4 Inductive setoid universe -- 5 Conclusions and further work -- References -- Nominal Equational Problems -- 1 Introduction -- 2 Background -- 3 Nominal Equational Problems -- 4 A rule-based procedure -- 4.1 Simplification Rules -- 4.2 Soundness and Preservation of Solutions -- 4.3 Termination -- 5 Nominal Equational Solved Forms -- 6 Conclusion -- References -- Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy -- 1 Introduction -- 2 Preliminaries -- 3 The cut-off problem for acyclic Petri nets -- 3.1 Characterizing acyclic systems with cut-offs -- 3.2 Polynomial time algorithm -- 4 The Scaling and Insertion lemmas -- 4.1 The Scaling Lemma -- 4.2 The Insertion Lemma -- 5 Polynomial time algorithm for the general case -- 5.1 Characterizing systems with cut-offs -- 5.2 Polynomial time algorithm -- 6 Symmetric rendez-vous protocols -- 7 Symmetric protocols with leaders -- 7.1 A non-deterministic polynomial time algorithm -- References -- Fixpoint Theory - Upside Down -- 1 Introduction -- 2 Lattices and MV-Algebras -- 3 Non-expansive Functions and Their Approximations -- 4 Proof Rules -- 5 (De)Composing Functions and Approximations -- 6 Applications -- 6.1 Termination Probability -- 6.2 Behavioural Metrics for Probabilistic Automata -- 6.3 Bisimilarity -- 7 Simple Stochastic Games -- 8 Conclusion -- References -- Most of'' leads to undecidability: Failure of adding frequencies to LTL -- 1 Introduction -- 1.1 Related work. 2 Preliminaries -- 3 Playing with Half Operator -- 4 Undecidability of LTL extensions -- 4.1 "Half of" meets the halting problem -- Fact 5 -- Fact 6 -- 6.1 Undecidability of model-checking -- 6.2 Most-Frequent Letter and Undecidability -- 6.3 Most-Frequent Letter: the reduction -- 7 Decidable variants -- 8 Two-Variable First-Order Logic with Majority -- 9 Conclusions -- References -- Combining Semilattices and Semimodules -- 1 Introduction -- 2 (Weak) Distributive laws -- 3 The Powerset and Semimodule Monads -- 4 The Weak Distributive Law δ : SP → PS -- 5 The Weak Lifting of P to EM(S) -- 5.1 Proof of Theorem 24 -- 6 The Composite Monad: an Algebraic Presentation -- 7 Conclusions: Related and Future Work -- References -- One-way Resynchronizability of Word Transducers -- 1 Introduction -- 2 Preliminaries -- 3 One-way resynchronizability -- 3.1 Regular resynchronizers -- 3.2 Main result -- 4 Proof overview for Theorem 1 -- 4.1 Flows and inversions -- 4.2 Dominant output intervals -- 5 Proof of Theorem 1 -- 6 Proof overview of Theorem 2 -- 7 Complexity -- 8 Conclusions -- References -- Fair Refinement for Asynchronous Session Types -- 1 Introduction -- 2 Refinement for Asynchronous Session Types -- 2.1 Preliminaries: Asynchronous Session Types -- 2.2 Fair Refinement for Asynchronous Session Types -- 2.3 Controllability for Asynchronous Session Types -- 3 Fair Asynchronous Session Subtyping -- 4 A Sound Algorithm for Fair Asynchronous Subtyping -- 5 Implementation -- 6 Related and Future Work -- References -- Running Time Analysis of Broadcast Consensus Protocols -- 1 Introduction -- 2 Preliminaries -- 3 Example: Majority -- 4 Comparison with other Models -- 4.1 Non-Deterministic Broadcast Protocols -- 4.2 Population Protocols -- 5 Protocols for Presburger Arithmetic -- 5.1 Linear Inequalities -- 5.2 Modulo Predicates and Boolean Combinations. 6 Protocols for all Predicates in ZPL -- References -- Leafy automata for higher-order concurrency -- 1 Introduction -- 2 Finitary Idealized Concurrent Algol (FICA) -- 3 Game semantics -- 4 Leafy automata -- 5 Local leafy automata (LLA) -- 6 From FICA to LA -- 7 Local FICA -- 8 From LA to FICA -- 9 Conclusion and further work -- References -- Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic -- 1 Introduction -- 2 Background in Abstract Rewriting -- 3 λ-calculi: CbN, CbV, and bang -- 3.1 Call-by-Name and Call-by-Value λ-calculi -- 3.2 Bang calculi -- 3.3 CbN and CbV translations into the bang calculus -- 4 The least-level strategy -- 4.1 Least-level reduction in bang calculi -- 4.2 Least-level for a bang calculus: examples. -- 4.3 Least-level for CbN and CbV λ-calculi -- 5 Embedding of CbN and CbV by level -- 6 Least-level factorization via bang calculus -- 6.1 Factorization of →β! in a bang calculus -- 6.2 Pure calculi and least-level normalization -- 6.3 Least-level Factorization, Modularly -- 7 Case study: non-deterministic λ-calculi -- 8 Conclusions and Related Work -- References -- Generalized Bounded Linear Logic and its Categorical Semantics -- 1 Introduction -- 2 Generalized Bounded Linear Logic -- 2.1 Indexing 2-Category -- 2.2 Formulas and Proofs -- 2.3 Complexity of Cut-Elimination in GBLL -- 3 Translation from Constrained BLL -- 3.1 Resource Polynomials and Constraints -- 3.2 Formulas and Inference Rules of CBLL -- 3.3 Translation into GBAL+ -- 4 Categorical Semantics for GBLL -- 4.1 Semantics of GBLL -- 4.2 Construction of an Indexed Linear Exponential Comonad -- 4.3 GBLL Semantics by Realizability Category -- 5 Conclusion and Related Work -- References -- Focused Proof-search in the Logic of Bunched Implications -- 1 Introduction -- 2 Re-presentations of BI -- 2.1 Traditional Syntax -- 2.2 Sequent Calculus. 2.3 Nested Calculus -- 3 A Focused System -- 3.1 Polarisation -- 3.2 Focused Calculus -- 3.3 Completeness of fBI -- 4 Conclusion -- References -- Interpolation and Amalgamation for Arrays with MaxDiff -- 1 Introduction -- 2 Formal Preliminaries -- 3 Arrays with MaxDiff -- 3.1 Our roadmap -- 4 Embeddings -- 5 Amalgamation -- 6 Satisfiability -- 7 An interpolation algorithm -- 8 When indexes are just a total order -- 9 Conclusions and further work -- References -- Adjoint Reactive GUI Programming -- Introduction -- The Language -- Formal Calculus -- Semantics -- Related and Future Work -- References -- On the Expressiveness of Büchi Arithmetic -- 1 Introduction -- 2 Preliminaries -- 3 The inexpressiveness of existential Büchi arithmetic -- 4 Expressive completeness of the ∑2-fragment of Büchi arithmetic -- 5 Existential Büchi arithmetic defines regular languages of polynomial growth -- 6 Conclusion -- References -- Parametricity for Primitive Nested Types -- 1 Introduction -- 2 The Calculus -- 2.1 Types -- 2.2 Terms -- 3 Interpreting Types -- 3.1 Interpreting Types as Sets -- 3.2 Interpreting Types as Relations -- 4 The Identity Extension Lemma -- 5 Interpreting Terms -- 6 Free Theorems for Nested Types -- 6.1 Consequences of Naturality -- 6.2 The Abstraction Theorem -- 7 Conclusion and Directions for Future Work -- References -- The Spirit of Node Replication -- 1 Introduction -- 2 A Calculus for Node Replication -- 3 Operational Properties -- 4 Encoding Evaluation Strategies -- 4.1 Call-by-name -- 4.2 Call-by-need -- 5 A Type System for the λR-calculus -- 6 Observational Equivalence -- 7 Related Works and Conclusion -- References -- Nondeterministic and co-Nondeterministic Implies Deterministic, for Data Languages -- 1 Introduction -- 2 Data languages and register automata -- 3 Examples -- 4 Main results -- 5 Orbit-finite automata. 6 Proof of Theorem 1 -- 6.1 Examples -- 6.2 Proof of Lemma 1 -- 7 Application to Unambiguous Register Automata -- 8 Proof of Theorem 2 -- 9 Final remarks -- References -- Certifying Inexpressibility -- 1 Introduction -- 2 Preliminaries -- 2.1 Transducers and Realizability -- 2.2 Automata -- 3 Refuting DBW-Recognizability -- 3.1 Complexity -- 3.2 Certifying DBW-Refutation -- 4 Separability and Approximations -- 4.1 Refuting Separability -- 4.2 Certificate-Guided Approximation -- 5 Other Classes of Deterministic Automata -- 6 Discussion and Directions for Future Research -- References -- A General Semantic Construction of Dependent Refinement Type Systems, Categorically -- 1 Introduction -- 2 Preliminaries -- 3 Lifting SCCompCs and Fibred Coproducts -- 3.1 Lifting SCCompCs -- 3.2 Lifting Fibred Coproducts -- 4 Lifting Monads on SCCompCs -- 5 Soundness -- 5.1 Underlying Type System -- 5.2 Predicate Logic -- 5.3 Refinement Type System -- 5.4 Semantics -- 6 Toward Recursion in Refinement Type Systems -- 6.1 Conway Operators -- 6.2 Recursion in the Underlying Type System -- 7 Related Work -- 8 Conclusion and Future Work -- References -- Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP -- 1 Introduction -- 2 Preliminaries -- 3 Characterizing Energy-Parity via Gain and Bailout -- 4 Bailout -- 5 Gain -- 6 The Main Results -- 7 Conclusion and Outlook -- References -- Nondeterministic Syntactic Complexity -- 1 Introduction -- 2 Preliminaries -- 3 Duality Theory of Semilattice Automata -- 4 Boolean Representations and Subatomic NFAs -- 5 Applications -- 5.1 Unary languages -- 5.2 Languages with a canonical state-minimal nfa -- 6 Conclusion and Future Work -- References -- A String Diagrammatic Axiomatisation of Finite-State Automata -- 1 Introduction -- 2 Syntax and semantics -- 3 Equational theory. 4 Encoding regular expressions and automata. |
isbn |
9783030719951 9783030719944 |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA267-268 |
callnumber-sort |
QA 3267 3268.5 |
genre |
Electronic books. |
genre_facet |
Electronic books. |
url |
https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6524970 |
illustrated |
Not Illustrated |
oclc_num |
1244535767 |
work_keys_str_mv |
AT kieferstefan foundationsofsoftwarescienceandcomputationstructures24thinternationalconferencefossacs2021heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2021luxembourgcityluxembourgmarch27april12021proceedings AT tassonchristine foundationsofsoftwarescienceandcomputationstructures24thinternationalconferencefossacs2021heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2021luxembourgcityluxembourgmarch27april12021proceedings |
status_str |
n |
ids_txt_mv |
(MiAaPQ)5006524970 (Au-PeEL)EBL6524970 (OCoLC)1244535767 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Lecture Notes in Computer Science Series ; v.12650 |
is_hierarchy_title |
Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. |
container_title |
Lecture Notes in Computer Science Series ; v.12650 |
author2_original_writing_str_mv |
noLinkedField |
_version_ |
1792331059515359232 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>11399nam a22004693i 4500</leader><controlfield tag="001">5006524970</controlfield><controlfield tag="003">MiAaPQ</controlfield><controlfield tag="005">20240229073839.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr cnu||||||||</controlfield><controlfield tag="008">240229s2021 xx o ||||0 eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9783030719951</subfield><subfield code="q">(electronic bk.)</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="z">9783030719944</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)5006524970</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL6524970</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1244535767</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">QA267-268.5</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Kiefer, Stefan.</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Foundations of Software Science and Computation Structures :</subfield><subfield code="b">24th International Conference, FOSSACS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, 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">2021.</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2021.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (587 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.12650</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- Constructing a universe for the setoid model -- 1 Introduction -- 1.1 Related work -- 2 MLTT^Prop -- 2.1 Formalization -- 3 Setoid model -- 3.1 Setoid model as a CwF -- 3.2 Setoid Type Theory -- 4 Universe of setoids -- 4.1 Inductive-recursive universes -- 4.2 Inductive-recursive setoid universe -- 4.3 Inductive-inductive setoid universe -- 4.4 Inductive setoid universe -- 5 Conclusions and further work -- References -- Nominal Equational Problems -- 1 Introduction -- 2 Background -- 3 Nominal Equational Problems -- 4 A rule-based procedure -- 4.1 Simplification Rules -- 4.2 Soundness and Preservation of Solutions -- 4.3 Termination -- 5 Nominal Equational Solved Forms -- 6 Conclusion -- References -- Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy -- 1 Introduction -- 2 Preliminaries -- 3 The cut-off problem for acyclic Petri nets -- 3.1 Characterizing acyclic systems with cut-offs -- 3.2 Polynomial time algorithm -- 4 The Scaling and Insertion lemmas -- 4.1 The Scaling Lemma -- 4.2 The Insertion Lemma -- 5 Polynomial time algorithm for the general case -- 5.1 Characterizing systems with cut-offs -- 5.2 Polynomial time algorithm -- 6 Symmetric rendez-vous protocols -- 7 Symmetric protocols with leaders -- 7.1 A non-deterministic polynomial time algorithm -- References -- Fixpoint Theory - Upside Down -- 1 Introduction -- 2 Lattices and MV-Algebras -- 3 Non-expansive Functions and Their Approximations -- 4 Proof Rules -- 5 (De)Composing Functions and Approximations -- 6 Applications -- 6.1 Termination Probability -- 6.2 Behavioural Metrics for Probabilistic Automata -- 6.3 Bisimilarity -- 7 Simple Stochastic Games -- 8 Conclusion -- References -- Most of'' leads to undecidability: Failure of adding frequencies to LTL -- 1 Introduction -- 1.1 Related work.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">2 Preliminaries -- 3 Playing with Half Operator -- 4 Undecidability of LTL extensions -- 4.1 "Half of" meets the halting problem -- Fact 5 -- Fact 6 -- 6.1 Undecidability of model-checking -- 6.2 Most-Frequent Letter and Undecidability -- 6.3 Most-Frequent Letter: the reduction -- 7 Decidable variants -- 8 Two-Variable First-Order Logic with Majority -- 9 Conclusions -- References -- Combining Semilattices and Semimodules -- 1 Introduction -- 2 (Weak) Distributive laws -- 3 The Powerset and Semimodule Monads -- 4 The Weak Distributive Law δ : SP → PS -- 5 The Weak Lifting of P to EM(S) -- 5.1 Proof of Theorem 24 -- 6 The Composite Monad: an Algebraic Presentation -- 7 Conclusions: Related and Future Work -- References -- One-way Resynchronizability of Word Transducers -- 1 Introduction -- 2 Preliminaries -- 3 One-way resynchronizability -- 3.1 Regular resynchronizers -- 3.2 Main result -- 4 Proof overview for Theorem 1 -- 4.1 Flows and inversions -- 4.2 Dominant output intervals -- 5 Proof of Theorem 1 -- 6 Proof overview of Theorem 2 -- 7 Complexity -- 8 Conclusions -- References -- Fair Refinement for Asynchronous Session Types -- 1 Introduction -- 2 Refinement for Asynchronous Session Types -- 2.1 Preliminaries: Asynchronous Session Types -- 2.2 Fair Refinement for Asynchronous Session Types -- 2.3 Controllability for Asynchronous Session Types -- 3 Fair Asynchronous Session Subtyping -- 4 A Sound Algorithm for Fair Asynchronous Subtyping -- 5 Implementation -- 6 Related and Future Work -- References -- Running Time Analysis of Broadcast Consensus Protocols -- 1 Introduction -- 2 Preliminaries -- 3 Example: Majority -- 4 Comparison with other Models -- 4.1 Non-Deterministic Broadcast Protocols -- 4.2 Population Protocols -- 5 Protocols for Presburger Arithmetic -- 5.1 Linear Inequalities -- 5.2 Modulo Predicates and Boolean Combinations.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">6 Protocols for all Predicates in ZPL -- References -- Leafy automata for higher-order concurrency -- 1 Introduction -- 2 Finitary Idealized Concurrent Algol (FICA) -- 3 Game semantics -- 4 Leafy automata -- 5 Local leafy automata (LLA) -- 6 From FICA to LA -- 7 Local FICA -- 8 From LA to FICA -- 9 Conclusion and further work -- References -- Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic -- 1 Introduction -- 2 Background in Abstract Rewriting -- 3 λ-calculi: CbN, CbV, and bang -- 3.1 Call-by-Name and Call-by-Value λ-calculi -- 3.2 Bang calculi -- 3.3 CbN and CbV translations into the bang calculus -- 4 The least-level strategy -- 4.1 Least-level reduction in bang calculi -- 4.2 Least-level for a bang calculus: examples. -- 4.3 Least-level for CbN and CbV λ-calculi -- 5 Embedding of CbN and CbV by level -- 6 Least-level factorization via bang calculus -- 6.1 Factorization of →β! in a bang calculus -- 6.2 Pure calculi and least-level normalization -- 6.3 Least-level Factorization, Modularly -- 7 Case study: non-deterministic λ-calculi -- 8 Conclusions and Related Work -- References -- Generalized Bounded Linear Logic and its Categorical Semantics -- 1 Introduction -- 2 Generalized Bounded Linear Logic -- 2.1 Indexing 2-Category -- 2.2 Formulas and Proofs -- 2.3 Complexity of Cut-Elimination in GBLL -- 3 Translation from Constrained BLL -- 3.1 Resource Polynomials and Constraints -- 3.2 Formulas and Inference Rules of CBLL -- 3.3 Translation into GBAL+ -- 4 Categorical Semantics for GBLL -- 4.1 Semantics of GBLL -- 4.2 Construction of an Indexed Linear Exponential Comonad -- 4.3 GBLL Semantics by Realizability Category -- 5 Conclusion and Related Work -- References -- Focused Proof-search in the Logic of Bunched Implications -- 1 Introduction -- 2 Re-presentations of BI -- 2.1 Traditional Syntax -- 2.2 Sequent Calculus.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">2.3 Nested Calculus -- 3 A Focused System -- 3.1 Polarisation -- 3.2 Focused Calculus -- 3.3 Completeness of fBI -- 4 Conclusion -- References -- Interpolation and Amalgamation for Arrays with MaxDiff -- 1 Introduction -- 2 Formal Preliminaries -- 3 Arrays with MaxDiff -- 3.1 Our roadmap -- 4 Embeddings -- 5 Amalgamation -- 6 Satisfiability -- 7 An interpolation algorithm -- 8 When indexes are just a total order -- 9 Conclusions and further work -- References -- Adjoint Reactive GUI Programming -- Introduction -- The Language -- Formal Calculus -- Semantics -- Related and Future Work -- References -- On the Expressiveness of Büchi Arithmetic -- 1 Introduction -- 2 Preliminaries -- 3 The inexpressiveness of existential Büchi arithmetic -- 4 Expressive completeness of the ∑2-fragment of Büchi arithmetic -- 5 Existential Büchi arithmetic defines regular languages of polynomial growth -- 6 Conclusion -- References -- Parametricity for Primitive Nested Types -- 1 Introduction -- 2 The Calculus -- 2.1 Types -- 2.2 Terms -- 3 Interpreting Types -- 3.1 Interpreting Types as Sets -- 3.2 Interpreting Types as Relations -- 4 The Identity Extension Lemma -- 5 Interpreting Terms -- 6 Free Theorems for Nested Types -- 6.1 Consequences of Naturality -- 6.2 The Abstraction Theorem -- 7 Conclusion and Directions for Future Work -- References -- The Spirit of Node Replication -- 1 Introduction -- 2 A Calculus for Node Replication -- 3 Operational Properties -- 4 Encoding Evaluation Strategies -- 4.1 Call-by-name -- 4.2 Call-by-need -- 5 A Type System for the λR-calculus -- 6 Observational Equivalence -- 7 Related Works and Conclusion -- References -- Nondeterministic and co-Nondeterministic Implies Deterministic, for Data Languages -- 1 Introduction -- 2 Data languages and register automata -- 3 Examples -- 4 Main results -- 5 Orbit-finite automata.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">6 Proof of Theorem 1 -- 6.1 Examples -- 6.2 Proof of Lemma 1 -- 7 Application to Unambiguous Register Automata -- 8 Proof of Theorem 2 -- 9 Final remarks -- References -- Certifying Inexpressibility -- 1 Introduction -- 2 Preliminaries -- 2.1 Transducers and Realizability -- 2.2 Automata -- 3 Refuting DBW-Recognizability -- 3.1 Complexity -- 3.2 Certifying DBW-Refutation -- 4 Separability and Approximations -- 4.1 Refuting Separability -- 4.2 Certificate-Guided Approximation -- 5 Other Classes of Deterministic Automata -- 6 Discussion and Directions for Future Research -- References -- A General Semantic Construction of Dependent Refinement Type Systems, Categorically -- 1 Introduction -- 2 Preliminaries -- 3 Lifting SCCompCs and Fibred Coproducts -- 3.1 Lifting SCCompCs -- 3.2 Lifting Fibred Coproducts -- 4 Lifting Monads on SCCompCs -- 5 Soundness -- 5.1 Underlying Type System -- 5.2 Predicate Logic -- 5.3 Refinement Type System -- 5.4 Semantics -- 6 Toward Recursion in Refinement Type Systems -- 6.1 Conway Operators -- 6.2 Recursion in the Underlying Type System -- 7 Related Work -- 8 Conclusion and Future Work -- References -- Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP -- 1 Introduction -- 2 Preliminaries -- 3 Characterizing Energy-Parity via Gain and Bailout -- 4 Bailout -- 5 Gain -- 6 The Main Results -- 7 Conclusion and Outlook -- References -- Nondeterministic Syntactic Complexity -- 1 Introduction -- 2 Preliminaries -- 3 Duality Theory of Semilattice Automata -- 4 Boolean Representations and Subatomic NFAs -- 5 Applications -- 5.1 Unary languages -- 5.2 Languages with a canonical state-minimal nfa -- 6 Conclusion and Future Work -- References -- A String Diagrammatic Axiomatisation of Finite-State Automata -- 1 Introduction -- 2 Syntax and semantics -- 3 Equational theory.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4 Encoding regular expressions and automata.</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">Tasson, Christine.</subfield></datafield><datafield tag="776" ind1="0" ind2="8"><subfield code="i">Print version:</subfield><subfield code="a">Kiefer, Stefan</subfield><subfield code="t">Foundations of Software Science and Computation Structures</subfield><subfield code="d">Cham : Springer International Publishing AG,c2021</subfield><subfield code="z">9783030719944</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=6524970</subfield><subfield code="z">Click to View</subfield></datafield></record></collection> |