Mathematics of Program Construction

Name: Mathematics of Program Construction | 11th International Conference, MPC 2012, Madrid, Spain, June 25-27, 2012, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

11th International Conference, MPC 2012, Madrid, Spain, June 25-27, 2012, Proceedings

Jeremy Gibbons Pablo Nogueira(Herausgeber*in)

Springer (Verlag)

Erschienen am 21. Juni 2012

X, 363 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-31113-0 (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
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

Systemvoraussetzungen

Als PDF speichern Als Link merken