Foundations of Software Science and Computational Structures

Name: Foundations of Software Science and Computational Structures | 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26--April 3, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26--April 3, 2011, Proceedings

Martin Hofmann(Herausgeber*in)

Springer (Verlag)

Erschienen am 14. März 2011

XV, 473 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-19805-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

Title
Preface
Organization
Table of Contents
The Search for Structure in Quantum Computation
Introduction
Strange Features of Quantum Mechanics
Categorical Quantum Mechanics and Graphical Calculi
Measurement-Based Computing
Topological Quantum Computing
References
Coalgebra and Computability
Coalgebraic Walks, in Quantum and Turing Computation
Introduction
Three Monads for Computation Types
Walk the Walk
Non-deterministic Walks
Probabilistic Walks
Quantum Walks
A Coalgebraic/Monadic Description of Quantum Walks
Reversibility of Computations
Summary, So Far
Turing Machines as Coalgebras
Conclusions
References
Similarity Quotients as Final Coalgebras
Introduction
Mathematical Preliminaries
Relators
Relators and Simulation
Relators Preserving Binary Composition
Further Examples of Relators
Theory of Simulation and Final Coalgebras
QF-Coalgebras
Extensional Coalgebras
Relating F-Coalgebras and QF-Coalgebras
Beyond Similarity
Multiple Relations
Constraints
Generalized Theory of Simulation and Final Coalgebras (Sketch)
References
What Do Reversible Programs Compute?
Introduction
Reversible Triple-Format Turing Machines
Semantics for Turing Machines
Foundations of Reversible Computing
Inversion
Reversibilization
Reversible Updates
Robustness
Exact Computational Expressiveness of the RTMs
Universality
r-Turing Completeness
Related Work
Conclusion
References
Type Theory
Irrelevance in Type Theory with a Heterogeneous Equality Judgement
Introduction and Related Work
Irrelevant Intensional Type Theory
Algorithmic Equality
A Universal Kripke Model for IITT
An Induction Measure
A Heterogeneously Typed Kripke Logical Relation
Validity in the Model
Meta-theoretic Consequences of the Model Construction
Extensions
Conclusions
References
When Is a Type Refinement an Inductive Type?
Introduction
Inductive Types and F-Algebras
A Framework for Refinement
Truth and Comprehension
Indexed Coproducts and Indexed Products
Liftings
From Liftings to Refinements
Some Specific Refinements
Starting with Already Indexed Types
Partial Refinement
Conclusions, Applications, Related and Future Work
References
Complexity of Strongly Normalising $\lambda$-Terms via Non-idempotent Intersection Types
Introduction
Syntax and Typing
Lambda Calculus with Klop's Extension
Intersection Types and Contexts
Typing System and Its Basic Properties
Soundness and Completeness of the Typing System w.r.t. Strong Normalisation
Soundness
Completeness
Corollaries
Optimal and Principal Typing
Optimal Typing
Principal-Optimal Typing Trees
Complexity
Complexity Result for Church-Klop's I
Complexity Result for Pure -Calculus
Conclusion
References
Realizability and Parametricity in Pure Type Systems
Introduction
The First Level
The Second Level
Structure of P2
Strong Normalization
Parametricity
Realizability
The Third Level
Extensions
Inductive Definitions
Program Extraction and Computational Irrelevance
Related Work and Conclusion
References
Process Calculi
Sound Bisimulations for Higher-Order Distributed Process Calculus
Introduction
Background
Our Contribution
Overview of the Paper
Higher-Order -Calculus with Passivation
Syntax
Labelled Transitions System
Environmental Bisimulations of HOP
Examples
Discussion and Future Work
References
Deriving Labels and Bisimilarity for Concurrent Constraint Programming
Background
Constraint Systems
Syntax
Reduction Semantics
Observational Equivalence
Saturated Bisimilarity for ccp
Saturated Barbed Bisimilarity
Correspondence with Observational Equivalence
Labeled Semantics
Strong and Weak Bisimilarity
Conclusions, Related and Future Work
References
Ordinal Theory for Expressiveness of Well Structured Transition Systems
Introduction
Preliminaries and WSTS
A Method for Comparing WSTS
A New Tool: Order Reflections
Expressiveness of WSTS and Order Reflections
Self-witnessing WSTS Classes
How to Prove the Non-existence of Reflections?
Vector Addition Systems and Lossy Channel Systems
Vector Addition Systems and Petri Nets
Lossy Channel Systems
Petri Nets Extensions with Data
Conclusion and Perspectives
References
Automata Theory
Alternation Elimination for Automata over Nested Words
Introduction
Preliminaries
Alternation-Elimination Scheme
Reduction to Complementation
Inherited Properties
Instances for Automata over Nested Words
Automata over Nested Words
Complementing Existential co-Büchi Automata
Alternation Elimination for Parity Automata
Applications and Concluding Remarks
References
Co-B$\"{u}$ching Them All
Introduction
Preliminaries
Translating to NCW
From NSW to NCW
From NRW and NMW to NCW
Translating to DCW
Applications
Discussion
References
Minimizing Deterministic Lattice Automata
Introduction
Preliminaries
Lattices and Lattice Automata
Minimizing LDFAs
Minimizing General LDFA
Minimizing an LDFA over a Fully Ordered Lattice
References
Regularity and Context-Freeness over Word Rewriting Systems
Introduction
Derivation Decomposition
Notations
Preservation Properties
Decomposition
Applications
Prefix, Suffix and Bifix Systems
Left-to-Right Derivation
Tagged and Tag-Adding Systems
Conclusion
References
Quantitative Robustness Analysis of Flat Timed Automata
Introduction
Definitions
Timed Automata, Zones
Parametric Objects
Symbolic Computations Using (Parametric) Zones
The Enlarged Reachability Set Reach(A)
Parametric Computation of Reach( A())
Representing Constraints as a Graph
Accelerating Computations of Greatest Fixpoints
Parametric Forward Analysis with Acceleration
Quantitative Safety
Conclusion
References
A Game Approach to Determinize Timed Automata
Introduction
Preliminaries
Timed Automata
Existing Approaches to the Determinization of TAs
A Game Approach
Definition of the Game
Properties of the Strategies
Choosing a Good Losing Strategy
Extension to -Transitions and Invariants
Comparison with Existing Methods
Comparison with KT-fmsd09
Comparison with BBBB-icalp09
Comparison of the Extension with -Transition and Invariants
Conclusion
References
A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes
Introduction
Preliminaries
The New Model Checking Algorithm
Main Idea
Expansion Relations
Type Generation Rules
Model Checking Algorithm
Correctness of the Algorithm
Experiments
Related Work
Conclusion
References
Church Synthesis Problem for Noisy Input
Introduction
Definitions
Games with Errors
Games with Detected Errors
Games with Undetected Errors
Regular Games with Detected Errors
Regular Games with Undetected Errors
Mean-Payoff Games with Errors
Multidimensional Mean-Payoff Games
Conclusion and Further Work
References
Probabilistic Modal $\mu$-Calculus with Independent Product
Introduction
Background Definitions and Notation
The Logic pL
Stochastic Tree Games
Game Semantics of pL
Inductive Characterization of the Objective of GX.F
Proof of Theorem 1
References
Semantics
A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces
Introduction
A Calculus of Capabilities
Hereditarily Monotonic Recursive Worlds
Step-Indexed Possible World Semantics of Capabilities
Generalized Frame and Anti-frame Rules
Conclusion and Future Work
References
A Modified GoI Interpretation for a Linear Functional Programming Language and Its Adequacy
Introduction
A Linear Functional Programming Language LFP and Its Operational Semantics
GoI Interpretation of LFP
Graphical Presentation of Partial Maps
The Standard GoI Interpretation
Modified GoI Interpretation
Deriving the Modification from a Realizability Interpretation
Interpretation of the Untyped Linear Lambda Calculus
Admissible Pers and Strict Morphisms
Interpretation of Recursion in Mackie Style
Proof of Soundness and Adequacy
References
Estimation of the Length of Interactions in Arena Game Semantics
Introduction
Arena Game Semantics
Arenas and Plays
Classes of Strategies
Size of Strategies and Interactions
Pointer Structures and Rewriting
Nd(n,p) as a Bound for Pointer Structures
Agents
Simulation of Visible Pointer Structures
Length of Interactions
Upper Bound
Lower Bound
Application to Head Linear Reduction
Conclusion and Future Work
References
Synchronous Game Semantics via Round Abstraction
Introduction
Basic Syntactic Control of Interference
Syntax
Relational Semantics
Polarised Trace Semantics
A Trace Model of Processes
A Polarised Trace Model of SCI
Round Abstraction
Synchronous Game Semantics
Discussion
Conclusion
References
Binding
Freshness and Name-Restriction in Sets of Traces with Names
Introduction
Nominal Preliminaries
The Planes of a Set
Basic Theory of Planes
Positive Planes
-Restriction on Nominal Sets
Nominal Languages
Nominal Kleene Algebra
LA Is Equal to LA
Conclusions
References
Polymorphic Abstract Syntax via Grothendieck Construction
Introduction
Background
Algebras in SetF for Abstract Syntax with Binding
Algebras in (SetF "3223379 U)U for Typed Abstract Syntax with Binding
Second-Order Polymorphic Abstract Syntax
System F
Modelling Syntax of F
General Signature
General Syntax Rules
Higher-Order Polymorphic Abstract Syntax
System F"121
Modelling Syntax of F"121
General Signature
General Syntax Rules
On Substitutions and Future Work
References
Security
Asymptotic Information Leakage under One-Try Attacks
Introduction
Notations and Preliminary Notions
Probability of Error, Leakage, Indistinguishability
Bounds and Asymptotic Behaviour
Examples
Sequential Observations and Hidden Markov Models
Conclusion and Further Work
References
A Trace-Based View on Operating Guidelines
Introduction
Preliminaries
Open Nets
Environments
Trace Semantics for Deadlock Freedom
Stop-Dead Semantics
Coincidence with Accordance
Trace Semantics for Deadlock Freedom and Boundedness
Bounded Stop-Dead Semantics
Coincidence with b-Accordance and Nonredundancy
Full Abstractness
Deciding bsd-Refinement
Comparing bsd-Semantics and Operating Guidelines
Deriving an Operating Guideline from the bsd-Semantics
Deriving bsd-Semantics from Operating Guidelines
Accordance Check with Operating Guidelines
Conclusions
References
Program Analysis
HTML Validation of Context-Free Languages
Introduction
Outline of the Paper
Example
Related Work
Parsing HTML Documents
A Model of HTML Parsing
Parsing Context-Free Sets of Documents
Generating Constraints
Solving Constraints
Example
Experimental Results
Conclusion
References
On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks
Introduction
Preliminaries on Graphs
Ad Hoc Networks
Configurations with Bounded Diameter
Maximal Clique Graphs with Bounded Paths
Ackermann-Hardness of cover in BPCn
Broadcast vs. Unicast Communication
Conclusions
References
The Reduced Product of Abstract Domains and the Combination of Decision Procedures
Introduction
Syntax and Semantics of Programs
Syntax
Interpretations
Multi-interpreted Program Scmantics
Algebraic Abstract Domains
Soundness and Completeness of Abstract Semantics
Abstractions between Multi-interpretations
Theories and Models
Logical Abstract Domains
Observational Semantics
Observable Properties of Multi-interpreted Programs
Soundness of the Abstraction of Observation Properties
Observational Extension
Iterated Reduction and Reduced Product
Observational Reduced Product
The Nelson-Oppen Combination Procedure
Formula Purification
Formula Reduction
Formula Satisfiability
Reduced Product of Logical and Algebraic Abstract Domains
Combining Logical and Algebraic Abstract Domains
Program Purification
Related Work
Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken