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.
Author(s): Roland Backhouse, Wei Chen, João F. Ferreira (auth.), Claude Bolduc, Jules Desharnais, Béchir Ktari (eds.)
Series: Lecture Notes in Computer Science 6120 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Pages: 427
Tags: Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Software Engineering; Programming Languages, Compilers, Interpreters; Antibodies; Artificial Intelligence (incl. Robotics)
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 -
