Algebra and Coalgebra in Computer Science

Name: Algebra and Coalgebra in Computer Science | 4th International Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

4th International Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011, Proceedings

Andrea Corradini Bartek Klin Corina Cîrstea(Herausgeber*in)

Springer (Verlag)

Erschienen am 27. August 2011

XI, 420 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-22944-2 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken