Mathematics of Program Construction
11th International Conference, MPC 2012, Madrid, Spain, June 25-27, 2012, Proceedings
Published on 21. June 2012
X, 363 pages
978-3-642-31113-0 (ISBN)
Description
This book constitutes the refereed proceedings of the 11th International Conference on Mathematics of Program Construction, MPC 2012, held in Madrid, Spain, in June 2012. The 13 revised full papers presented together with three invited talks were carefully reviewed and selected from 27 submissions. The papers are organized in topical sections on security and information flow, synchronous and real-time systems, algorithms and games, program calculi, tool support, algebras and datatypes, and categorical functional programming.
More details
Other editions
Additional editions
Jeremy Gibbons | Pablo Nogueira
Mathematics of Program Construction
11th International Conference, MPC 2012, Madrid, Spain, June 25-27, 2012, Proceedings
Book
06/2012
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Invited Talks
- Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs
- References
- The Laws of Programming Unify Process Calculi
- Introduction
- Laws of Programming
- Lemmas
- Calculi of Programming
- Hoare Logic
- The Milner Calculus
- Natural Semantics
- Related Work
- Further Work
- Unification in Science and Engineering
- Conclusion
- References
- The Geometry of Synthesis
- References
- Security and Information Flow
- Scheduler-Independent Declassification
- Introduction
- Preliminaries
- Multi-threaded Programs
- Exemplary Programming Language
- Attacker Model and Security Policies
- Auxiliary Concepts for Relations
- Declassification in the Presence of Scheduling
- Escape Hatches and Immediate Declassification Steps
- The Security Conditions WHATs
- The Security Conditions WHAT&WHEREs
- Meta-properties of the Scheduler-Specific Security Properties
- Secure Declassification for Multi-threaded Programs
- Scheduler-Independent WHAT-Security
- Scheduler-Independent WHAT&WHERE-Security
- Security Type System
- Related Work
- Conclusion
- References
- Elementary Probability Theory in the Eindhoven Style
- Context and Motivation
- The Eindhoven Quantifier Notation, and Our Extension
- Discrete Distributions as Enumerations
- Finite Discrete Distributions as a Type
- The Support of a Distribution
- Specialised Notation for Uniform Distributions
- General Notation for Distribution Enumerations
- The Support of a Distribution is a Subset of Its Base
- Specialised Infix Notations for Making Distributions
- Comparison with Conventional Notation
- Expected Values over Discrete Distributions
- Definition of Expected Value as Average
- The Probability of a Subset Rather Than of a Single Element
- Abbreviation Conventions
- Example of Expected Value: Dice at the Fairground
- Comparison with Conventional Notation
- Discrete Distributions as Comprehensions
- Definition of Distribution Comprehensions
- Examples of Distribution Comprehensions
- Comparison with Conventional Notation
- Conditional Distributions
- Definition of Conditional Distributions
- Example of Conditional Distributions
- Comparison with Conventional Notation
- Conditional Expectations
- Definition of Conditional Expectations
- Conventions for Default Range
- Examples of Conditional Expectations
- Comparison with Conventional Notation
- Belief Revision: A Priori and A Posteriori Reasoning
- A-Priori and A-Posteriori Distributions in Conventional Style: Introduction and First Example
- Definition of a Posteriori Expectation
- Second Example of Belief Revision: Bertrand's Boxes
- Third Example of Belief Revision: The Reign in Spain
- General Distribution Comprehensions
- Comparison with Conventional Notation
- Use in Computer Science for Program Semantics
- ``Elementary'' Can Still Be Intricate
- Case Study: Quantitative Noninterference Security
- Comparison with Conventional Notation
- Comparison with Qualitative Noninterference Security
- Monadic Structures and Other Related Work
- Summary and Prospects
- References
- Synchronous and Real-Time Systems
- Scheduling and Buffer Sizing of n-Synchronous Systems
- Introduction
- The Lucy-n Language
- Clock Calculus
- Algebra of Ultimately Periodic Words
- Ultimately Periodic Binary Words
- Adaptability Relation
- Buffer Size
- Sampled Clocks
- Adaptability Constraints Resolution Algorithm
- Constraint System Simplification
- Constraint System Solving
- Guiding the Resolution Algorithm
- Correctness, Completeness and Complexity
- Comparison with Previous Resolution Algorithms
- Conclusion
- References
- Deriving Real-Time Action Systems Controllers from Multiscale System Specifications
- Introduction
- Motivating Example
- Contributions and Overview
- Related Work
- Background Theory
- Interval Predicates
- Evaluating State Predicates over an Interval
- Chop and Iteration
- ILTL
- Action Systems with Time Bands
- Time Bands
- Actions
- Action Systems
- Parallel Composition
- Deriving Action System Controllers
- Enforced Properties
- Action System Refinement
- Hardware/Software Interaction
- Example: Two-Tank Pump System
- Formulae Transformation
- Action Calculation
- Discharge Enforced Properties on Actions
- Conclusions
- References
- Algorithms and Games
- Calculating Graph Algorithms for Dominance and Shortest Path
- Introduction
- Background
- Notation
- Basics of Domain Theory and Abstract Interpretation
- Elements of Relational Algebra
- Calculating a Dominance Algorithm
- Graphs and Finite Paths
- Dominance in Finite Paths
- A Galois Connection between Sets of Finite Paths and Dominance Relations
- A Dominance Computation Functional
- Dominance Equations
- Complexity
- Calculating a Shortest Path Algorithm
- Weighted Graphs and Paths
- The Single-Source Shortest Path Property for Finite Paths
- A Galois Connection between Sets of Finite Paths and the Shortest Path Weights
- A Shortest-Path Functional
- Complexity
- Computing the Shortest Paths
- Related Work
- Conclusion
- References
- First-Past-the-Post Games
- Preliminaries
- First-Past-the-Post Games
- Prefix-Free Languages
- Block Patterns and Penney-Ante Games
- Equations in Languages
- Solov'ev's Equation and Conway's Equation
- Uniqueness
- Conclusion
- References
- Program Calculi
- Reverse Exchange for Concurrency and Local Reasoning
- Introduction
- Basic Definitions and Properties
- Compatibility and the Reverse Exchange Law
- Hoare Triples and the Concurrency Rule
- Another Concurrency Rule
- Locality and the Frame Rule
- Dual Correctness Triples
- Further Variations
- Conclusion
- References
- Unifying Correctness Statements
- Introduction
- Models
- Partial Correctness
- Total Correctness
- General Correctness
- Extended Designs
- Finite, Infinite and Aborting Executions
- Summary
- Relative Domain Semirings
- Relative Domain
- Relative Modal Operators
- Iteration
- Correctness Statements
- Tests
- Preconditions
- While-Programs
- Correctness Calculus
- Pre-post Specifications
- Conclusion
- References
- Tool Support
- Dependently Typed Programming Based on Automated Theorem Proving
- Introduction
- Calculus of Constructions
- An Extended Calculus
- Automated Theorem Proving Technology
- ATP Integration
- Proof Reconstruction
- Proof Experiments
- Related Work
- Conclusion and Future Work
- References
- Algebras and Datatypes
- An Algebraic Calculus of Database Preferences
- Introduction
- Types and Tuples
- Typed Tuples
- Typed Relations
- Inverse Image and Maximal Elements
- An Algebraic Calculus
- Semirings
- Representing Types
- Join Algebras
- Representation of Preferences
- Maximal Element Algebra
- Basic Definitions and Results
- Basic Applications
- Prefilters
- Complex Preferences
- Complex Preferences as Typed Relations
- Maximality for Complex Preferences
- Equivalence of Preference Terms
- Conclusion and Outlook
- References
- Modular Tree Automata
- Introduction
- Bottom-Up Tree Acceptors
- Deterministic Bottom-Up Tree Acceptors
- Algebras and Catamorphisms
- Bottom-Up State Transition Functions
- Making Tree Automata Modular
- Product Automata
- Compositional Data Types
- Bottom-Up Tree Transducers
- Deterministic Bottom-Up Tree Transducers
- Contexts in Haskell
- Bottom-Up Transduction Functions
- Tree Homomorphisms
- Combining Tree Homomorphisms with State Transitions
- Refining Dependent Bottom-Up State Transition Functions
- Top-Down Automata
- Deterministic Top-Down Tree Transducers
- Top-Down Transduction Functions
- Top-Down State Transition Functions
- Making Top-Down State Transition Functions Modular
- Bidirectional State Transitions
- Avoiding the Problem
- A Direct Implementation
- Discussion
- References
- Categorical Functional Programming
- Constructing Applicative Functors
- Introduction
- Applicative Functors
- Lax Monoidal Functors
- Weak Commutativity
- Fixed Points, Limits and Colimits
- Limits
- Sums
- Generalized Semi-direct Products
- Existentials and Coends
- Left Kan Extensions
- The General Case
- Conclusion
- References
- Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick
- Introduction
- Background
- Adjunction
- String Diagram
- Monad
- Kan Extension-Specification
- Codensity Monad
- Absolute Kan Extension-Implementation
- Kan Extension as an End-Implementation
- Background: Power
- Background: End
- End Formula
- Examples
- Identity Monad
- State Monad
- Free Monad of a Functor
- List Monad
- Related Work
- Conclusion
- References
- Author Index
