Mathematics of Program Construction : 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010, Proceedings

This book constitutes the refereed proceedings of the 10th International Conference on Mathematics of Program Construction, MPC 2010, held in Québec City, Canada in June 2010. The 19 revised full papers presented together with 1 invited talk and the abstracts of 2 invited talks were carefully reviewed and selected from 37 submissions. The focus is on techniques that combine precision with conciseness, enabling programs to be constructed by formal calculation. Within this theme, the scope of the series is very diverse, including programming methodology, program specification and transformation, program analysis, programming paradigms, programming calculi, programming language semantics, security and program logics. Front Matter....Pages - The Algorithmics of Solitaire-Like Games....Pages 1-18 Compositionality of Secure Information Flow....Pages 19-19 Process Algebras for Collective Dynamics....Pages 20-21 On Automated Program Construction and Verification....Pages 22-41 The Logic of Large Enough....Pages 42-57 Dependently Typed Grammars....Pages 58-79 Abstraction of Object Graphs in Program Verification....Pages 80-99 Subtyping, Declaratively....Pages 100-118 Compositional Action System Derivation Using Enforced Properties....Pages 119-139 Designing an Algorithmic Proof of the Two-Squares Theorem....Pages 140-156 Partial, Total and General Correctness....Pages 157-177 Unifying Theories of Programming That Distinguish Nontermination and Abort....Pages 178-194 Adjoint Folds and Unfolds....Pages 195-228 An Abstract Machine for the Old Value Retrieval....Pages 229-247 A Tracking Semantics for CSP....Pages 248-270 Matrices as Arrows!....Pages 271-287 Lucy-n: a n-Synchronous Extension of Lustre....Pages 288-309 Sampling, Splitting and Merging in Coinductive Stream Calculus....Pages 310-330 Generic Point-free Lenses....Pages 331-352 Formal Derivation of Concurrent Garbage Collectors....Pages 353-376 Temporal Logic Verification of Lock-Freedom....Pages 377-396 Gradual Refinement....Pages 397-425 Back Matter....Pages -