9. MPC 2008: Marseille, France

• Ralf Hinze:
  Exploiting Unique Fixed Points. 1
  
• Barry Jay, Simon L. Peyton Jones:
  Scrap Your Type Applications. 2-27
  
• Greg Morrisett:
  Programming with Effects in Coq. 28
  
• Andreas Abel, Thierry Coquand, Peter Dybjer:
  Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. 29-56
  
• Roland Carl Backhouse:
  The Capacity-CTorch Problem. 57-78
  
• Roland Carl Backhouse, João F. Ferreira:
  Recounting the Rationals: Twice!. 79-91
  
• Richard S. Bird:
  Zippy Tabulations of Recursive Functions. 92-109
  
• Jeremy Gibbons:
  Unfolding Abstract Datatypes. 110-133
  
• Roland Glück, Bernhard Möller:
  Circulations, Fuzzy Relations and Semirings. 134-152
  
• William L. Harrison, Gerard Allwein, Andy Gill, Adam M. Procter:
  Asynchronous Exceptions as an Effect. 153-176
  
• Dexter Kozen, Wei-Lung Dustin Tseng:
  The Böhm-Jacopini Theorem Is False, Propositionally. 177-192
  
• Ralf Lämmel, Ondrej Rypacek:
  The Expression Lemma. 193-219
  
• Ralph Matthes:
  Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening. 220-242
  
• Larissa Meinicke, Ian J. Hayes:
  Probabilistic Choice in Refinement Algebra. 243-267
  
• Shin-Cheng Mu, Hsiang-Shang Ko, Patrik Jansson:
  Algebra of Programming Using Dependent Types. 268-283
  
• Susumu Nishimura:
  Safe Modification of Pointer Programs in Refinement Calculus. 284-304
  
• Yann Régis-Gianas, François Pottier:
  A Hoare Logic for Call-by-Value Functional Programs. 305-335
  
• Michel Sintzoff:
  Synthesis of Optimal Control Policies for Some Infinite-State Transition Systems. 336-359
  
• Jules Desharnais, Georg Struth:
  Modal Semirings Revisited. 360-387
  
• Janis Voigtländer:
  Asymptotic Improvement of Computations over Free Monads. 388-403
  
• Andreas Witzel:
  Symmetric and Synchronous Communication in Peer-to-Peer Networks. 404-421