Algebra and Coalgebra in Computer Science
4th International Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011, Proceedings
Published on 27. August 2011
XI, 420 pages
978-3-642-22944-2 (ISBN)
Description
This book constitutes the refereed proceedings of the 4th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2011, held in Winchester, UK, in August/September 2011. The 21 full papers presented together with 4 invited talks were carefully reviewed and selected from 41 submissions. The papers report results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. They cover topics in the fields of abstract models and logics, specialized models and calculi, algebraic and coalgebraic semantics, and system specification and verification. The book also includes 6 papers from the CALCO-tools Workshop, colocated with CALCO 2011 and dedicated to tools based on algebraic and/or coalgebraic principles.
More details
Other editions
Additional editions
Andrea Corradini | Bartek Klin | Corina Cîrstea
Algebra and Coalgebra in Computer Science
4th International Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011, Proceedings
Book
08/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Intro
- Titlepage
- Preface
- Organization
- Table of Contents
- Invited Talks
- On the Statistical Thermodynamics of Reversible Communicating Processes
- Introduction
- Energy Landscaping
- Related Work
- Outline
- Probabilistic Reminders
- Timers and Chains
- Equilibrium
- Potentials
- Qualitative Semantics
- Memories and Transitions
- Near Acyclicity and Simplicity
- An Aside on Degenerate Sums
- Which Potential to Look for?
- Concurrent Potentials
- Total Stack Size Potential
- Total Synch Potential
- V1 vs. V0
- Explosive Growth
- Main Statement
- Lower Bound on the Potential
- Upper Bound on the Number of Traces
- Convergence
- Discussion
- Conclusion
- References
- Solving Fixed-Point Equations by Derivation Tree Analysis
- Introduction
- Polynomial Equations Over Semirings
- From Equations to Grammars
- Newton's Approximation
- Convergence of Newton's Method in Commutative Semirings
- Derivation Tree Analysis for Idempotent Semirings
- 1-bounded Semirings
- Star-distributive Semirings
- Conclusions
- References
- Abstract Local Reasoning for Program Modules
- References
- Infinite Computation, Co-induction and Computational Logic
- Introduction
- Coinduction and Logic Programming
- Model Checking with Co-LP
- Negation in Co-LP
- Modeling Complex Real-time Systems
- Pushdown ?-Automata and ?-Grammars
- Timed p-calculus
- Integrating Coinduction and Induction
- Stratified Co-LP: Applications and Limitations
- Towards Non-stratified Co-LP
- Conclusions
- References
- Contributed Papers
- From Corecursive Algebras to Corecursive Monads
- Introduction
- Corecursive Algebras
- Bloom Algebras
- Free Corecursive Algebras
- Corecursive Monads
- Free Corecursive Monad
- Conclusions and Further Work
- References
- A Categorical Semantics for Inductive-Inductive Definitions
- Introduction
- Examples of Inductive-Inductive Definitions
- Preliminaries and Notation
- Inductive-Inductive Definitions as Dialgebras
- A Category for Inductive-Inductive Definitions
- How to Exploit Initiality: An Example
- Relationship to Induction-Induction as Axiomatised in nordvallforsbergSetzer2010indind
- The Elimination Principle
- Warm-Up: A Generic Eliminator for an Inductive Definition
- The Generic Eliminator for an Inductive-Inductive Definition
- The Equivalence between Having an Eliminator and Being Initial
- Conclusions and Future Work
- References
- Finitary Functors: From Set to Preord and Poset
- Introduction
- Preliminaries
- From Set to Preord
- Extension and Lifting
- First Construction: Order on the Variables
- Second Construction: Order on the Operations
- Lifting T to T^ Using Relators
- Preorder on the Final Coalgebra
- Third Construction: Order the Variables and Operations
- From Preord to Poset
- Conclusion
- References
- Model Constructions for Moss' Coalgebraic Logic
- Introduction
- Preliminaries
- Moss' Logic and Its Axiomatization
- Moss' Logic
- The Derivation System M
- One-Step Soundness and Completeness
- A Finite Model Construction
- Strong Completeness
- References
- Relation Liftings on Preorders and Posets
- Introduction
- Monotone Relations
- The Functor (-) : Pre - Rel(Pre)
- Rel(Pre) as a Kleisli Category
- Relations as Spans
- Composition of Fibrations
- Exact Squares
- The Universal Property of (-) : Pre - Rel(Pre)
- The Extension Theorem
- Examples
- An Application: Moss's Coalgebraic Logic over Posets
- Conclusions
- References
- Model Checking Linear Coalgebraic Temporal Logics: An Automata-Theoretic Approach
- Introduction
- Preliminaries
- Automata-Based Characterisation of Maximal Traces
- Model Checking Linear Coalgebraic Temporal Logics
- Concluding Remarks
- References
- Refinement Trees: Calculi, Tools, and Applications
- Introduction
- The CASL Refinement Language: Syntax
- Refinement Trees
- The CASL Refinement Language: Semantics
- Proof Calculus for the CASL Refinement Language
- Checking Consistency of Refinement Specifications
- Conclusions
- References
- On the Fusion of Coalgebraic Logics
- Introduction
- Preliminaries
- Fusion and Transfer of Soundness and Consistency
- Transfer of Completeness
- Ersatz and Reconstruction
- Consistency Sets and Consistency Formulae
- Necessity Operators and Distances
- Generated Submodels
- Characteristic Sets and Formulae
- Transfer of Completeness
- Discussion and Future Work
- References
- Indexed Induction and Coinduction, Fibrationally
- Introduction
- Induction in a Fibrational Setting
- Fibrations in a Nutshell
- Fibrational Induction in Another Nutshell
- Coinduction
- Generic Coinduction for All Final Coalgebras
- Indexed Induction
- Indexed Coinduction
- The Equality Functor for U/I
- The Quotient Functor for U/I
- Conclusions, Related Work, and Future Work
- References
- Stone Duality for Nominal Boolean Algebraswith N
- Introduction
- Background on Nominal Sets and the Nps: currentpoint currentpoint translate scale neg exch neg exch translatetops: currentpoint currentpoint translate 1 div 1 div scale neg exch neg exch translate11to-1-quantifier
- Nominal Boolean Algebra with Nps: currentpoint currentpoint translate scale neg exch neg exch translatetops: currentpoint currentpoint translate 1 div 1 div scale neg exch neg exch translate11to-1
- The Nominal Powerset as an Algebra
- A Representation Theorem
- n-Filters
- The Canonical Extension -
- Nominal Stone Duality
- Conclusions
- References
- A Counterexample to Tensorability of Effects
- Introduction
- Monads vs. Large Lawvere theories
- Tensors and Tensor Algebras
- Existence of Tensor Products
- Nonexistence of Tensor Products
- Conclusion
- References
- The Microcosm Principle and Compositionality of GSOS-Based Component Calculi
- Introduction
- Structural Operational Semantics and Its Bialgebraic Modeling
- Parallel Composition of Coalgebras and the Microcosm Principle
- Microcosm Interpretation of Full GSOS Rules
- A Technical Challenge: State Spaces
- State Space Compatible with GSOS Rules
- GSOS Specification
- Requirements on State Spaces
- Term Lineage Graph (TLG)
- R-State Space
- Categorical GSOS Specification
- Copointed Functors and Copointed Coalgebras
- GSOS Rules, Categorically
- The Microcosm Interpretation of GSOS Rules
- Conclusions and Future Work
- References
- Bases as Coalgebras
- Introduction
- Comonads on Categories of Algebras
- Set-Theoretic Examples
- Complete Lattices
- Vector Spaces
- Order-Theoretic Examples
- Dcpos over Posets
- Frames over Semi-lattices
- Comonoids from Bases
- References
- A Coalgebraic Approach to Supervisory Control of Partially Observed Mealy Automata
- Introduction
- Preliminaries
- Notations
- Mealy Automata as $(1 + B ×-)^A$-coalgebras
- Moore Automata as $B × (-)^A$-coalgebras
- Finite Automata as $(1 + -)^A$-coalgebras
- Supervisory Control of Mealy Automata
- Coalgebraic Formulation of Supervisory Control
- Solution to the Supervisory Control Problem for Mealy Automata
- Modified Normal Relations
- Modified Normality
- Conclusion
- References
- Coalgebraic Semantics for Derivations in Logic Programming
- Introduction
- Parallel and-or Derivation Trees and Coalgebra
- Using Lawvere Theories to Model First-Order Signatures and Substitution
- Coalgebra on Categories of Lax Maps
- Coalgebraic Semantics for Arbitrary Logic Programs
- Conclusions and Further Work
- References
- Hybridization of Institutions
- Introduction
- Notation and Definitions
- A Method to Hybridize Arbitrary Institutions
- FOL as a Support to Hybrid Specification
- Conclusions and Further Work
- References
- Linearly-Used State in Models of Call-by-Value
- Introduction
- Source Calculus: Fine-Grained Call-by-Value
- Effect Theories
- Target Calculus: Enriched Call-by-Value
- The State-Passing Translation
- Categorical Models
- Monad Models of the Fine-Grained Call-by-Value Calculus
- Enriched Call-by-Value Models
- From Enriched Models to Monad Models and Back
- Remark: Closed Freyd Categories
- Models and Comodels of Effect Theories
- Categories of Models and Full Completeness
- Full Completeness
- The Enriched Effect Calculus
- References
- Proving Safety Properties of Rewrite Theories
- Introduction
- Preliminaries
- Ground Stability
- Ground Invariance
- Strengthenings for Ground Invariance
- Maude's Invariant Analyzer
- Related Work
- Concluding Remarks
- References
- Generalized Product of Coalgebraic Hybrid Logics
- Introduction and Motivation
- Generalized Product of Coalgebras and Predicate Lifting
- Coalgebraic Semantics for Bi-Hybrid Language
- Generalized Product of Coalgebraic Hybrid Logics
- Pure Completeness for Coalgebraic Hybrid g-Product Logic
- Generalized Product of Strongly One-Step Complete Logics
- Generalized Product of Bounded Logics
- Generalized Product of Bounded and Non-bounded Logics
- Adding Downarrow Binders
- Conclusions and Future Work
- References
- Distributive-Law Semantics for Cellular Automata and Agent-Based Models
- Introduction
- Theory of Bialgebras
- Syntax
- Static Semantics
- Flat Semantics
- Context and Template
- Regular Contexts
- Compositional Contexts
- Behavior
- Distributive Law
- Equivalence
- Conclusion
- References
- Context-Free Languages, Coalgebraically
- Introduction
- Coalgebras and Deterministic Automata
- Context-Free Languages via Grammars
- A Coalgebraic Treatment of Context-Free Grammars
- Context-Free Languages via Equations
- Context-Free Expressions
- From Systems of Equations to Context-Free Expressions
- From Context-Free Expressions to Systems of Equations
- Discussion
- References
- CALCO Tools Workshop
- Preface to CALCO-Tools
- PREG Axiomatizer - A Ground Bisimilarity Checker for GSOS with Predicates
- Introduction
- Case Studies
- Discussion and Future Work
- References
- PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool
- Introduction
- Efficient Parallel Statistical Analysis Algorithms
- Implementation of PVeStA
- Experimental Evaluation
- Conclusion and Future Work
- References
- Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras
- Introduction
- Program Extraction in Minlog
- The Interactive Proof System Minlog
- Program Extraction
- Related Work
- Case Studies
- Algebras for Parsing
- Coalgebras for Exact Real Numbers
- References
- Tool Interoperability in the Maude Formal Environment
- Introduction
- MFE's Design and Main Features
- Case Study: Ground Coherence of the Bakery Protocol
- Future Work
- References
- WiCcA : LTS Generation Tool for Wire Calculus
- Introduction
- Running Example
- FeaturesofWiCcA
- Running WiCcA
- Future Work
- References
- SHACC: A Functional Prototyper for a Component Calculus
- Introduction
- A Components' Calculus
- TheSHACC Tool
- References
- Author Index
