Cover Image

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.

Bibliographic Details
Main Author: Kiefer, Stefan.
Other Authors: Tasson, Christine.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2021.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
Table of 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.

Similar Items