Mathematics of program construction : 9th international conference, MPC 2008, Marseille, France, July 15-18, 2008 : proceedings

Exploiting Unique Fixed Points.- Scrap Your Type Applications.- Programming with Effects in Coq.- Verifying a Semantic ??-Conversion Test for Martin-Lof Type Theory.- The Capacity-C Torch Problem.- Recounting the Rationals: Twice!.- Zippy Tabulations of Recursive Functions.- Unfolding Abstract Datatypes.- Circulations, Fuzzy Relations and Semirings.- Asynchronous Exceptions as an Effect.- The Bohm-Jacopini Theorem Is False, Propositionally.- The Expression Lemma.- Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening.- Probabilistic Choice in Refinement Algebra.- Algebra of Programming Using Dependent Types.- Safe Modification of Pointer Programs in Refinement Calculus.- A Hoare Logic for Call-by-Value Functional Programs.- Synthesis of Optimal Control Policies for Some Infinite-State Transition Systems.- Modal Semirings Revisited.- Asymptotic Improvement of Computations over Free Monads.- Symmetric and Synchronous Communication in Peer-to-Peer Networks.