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
Published on 14. March 2011
XV, 473 pages
978-3-642-19805-2 (ISBN)
Description
This book constitutes the refereed proceedings of the 14th International Conference on Foundations of Software Science and computational Structures, FOSSACS 2011, held in Saarbrücken, Germany, March 26-April 3, 2011, as part of ETAPS 2011, the European Joint Conferences on Theory and Practice of Software.
The 30 revised full papers presented together with one full-paper length invited talk were carefully reviewed and selected from 100 submissions. The papers are organized in topical sections on coalgebra and computability, type theory, process calculi, automata theory, semantics, binding, security, and program analysis.
More details
Other editions
Additional editions
Martin Hofmann
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
Book
03/2011
Springer
€53.49
Shipment within 7-9 days
Person
Content
- 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
