<div dir="ltr"><div>----------------------------------------------------------------------</div><div><br></div><div> CALL FOR PARTICIPATION</div><div><br></div><div> HOPE 2013</div>
<div><br></div><div> The 2nd ACM SIGPLAN Workshop on</div><div> Higher-Order Programming with Effects</div><div><br></div><div> September 28, 2013</div><div> Boston, Massachusetts</div>
<div> (the day after ICFP 2013)</div><div><br></div><div> <a href="http://hope2013.mpi-sws.org">http://hope2013.mpi-sws.org</a></div><div><br></div><div>----------------------------------------------------------------------</div>
<div><br></div><div>HOPE 2013 aims at bringing together researchers interested in the</div><div>design, semantics, implementation, and verification of higher-order</div><div>effectful programs. It will be *informal*, consisting of invited talks</div>
<div>and contributed talks on work in progress.</div><div><br></div><div><br></div><div>------------</div><div>Registration </div><div>------------</div><div><br></div><div>Web site: <a href="https://regmaster3.com/2013conf/ICFP13/register.php">https://regmaster3.com/2013conf/ICFP13/register.php</a></div>
<div><br></div><div>This is the registration site for ICFP 2013 and all the affiliated</div><div>workshops including HOPE 2013.</div><div><br></div><div><br></div><div>----------------</div><div>Workshop Program</div><div>
----------------</div><div><br></div><div>We received 20 high-quality submissions for talk proposals this year, </div><div>from which the program committee decided to accept 10 for presentation </div><div>at the workshop. The talks will be video-recorded, and the recordings </div>
<div>will be made available here after the workshop.</div><div><br></div><div>Also this year, the workshop will feature a special session in memory </div><div>of John Reynolds. The session will include talks from Olivier Danvy, </div>
<div>Robert Harper, Peter O'Hearn, and Uday Reddy, with a mixture of </div><div>scientific and personal reflections on John's life and work. This </div><div>special session is sponsored in part by a generous donation from </div>
<div>Microsoft Research.</div><div><br></div><div>Session 1: Concurrent Program Logics</div><div><br></div><div> 9:00 Impredicative Concurrent Abstract Predicates</div><div> Kasper Svendsen and Lars Birkedal</div>
<div> 9:30 Subjective Concurrent Protocol Logic</div><div> Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and </div><div> German Andres Delbianco</div><div> 10:00 Protocols for Protocols: Using Modal Separation Logic to Prove </div>
<div> Extrinsic Properties of Secure Communication </div><div> David Swasey, Derek Dreyer, Deepak Garg, Robert Harper, and </div><div> Aaron Turon</div><div> 10:30 Coffee Break</div><div><br></div><div>
Session 2: Semantics</div><div><br></div><div> 11:00 A Kripke Logical Relation for Affine Functions: </div><div> The Story of a Free Theorem in the Presence of Non-termination </div><div> Phillip Mates and Amal Ahmed</div>
<div> 11:30 Deconstructing General References via Game Semantics </div><div> Andrzej Murawski and Nikos Tzevelekos</div><div> 12:00 Linking Isn't Substitution </div><div> Jeremy Siek</div><div> 12:30 Lunch (NOTE: only one hour for lunch)</div>
<div><br></div><div>Session 3: Special Session in Memory of John Reynolds</div><div><br></div><div> 1:30 Olivier Danvy</div><div> 2:00 Robert Harper</div><div> 2:30 Peter O'Hearn</div><div> 3:00 Uday Reddy</div><div>
3:30 Coffee Break</div><div><br></div><div>Session 4: Types and Verification</div><div><br></div><div> 4:00 Refinement Types and Algebraic Effects </div><div> Danel Ahman</div><div> 4:30 Adventures in Knot-Tying while Verifying a Thread Library in Coq </div>
<div> Adam Chlipala</div><div> 5:00 The Ins and Outs of Iteration in Mezzo </div><div> Armael Gueneau, Francois Pottier, and Jonathan Protzenko</div><div> 5:30 Attacking the Imperative Relationship Update Problem </div>
<div> with Almost Everywhere Heap Invariants </div><div> Devin Coughlin and Bor-Yuh Evan Chang</div><div><br></div><div><br></div><div>---------------------</div><div>Goals of the Workshop</div><div>---------------------</div>
<div><br></div><div>A recurring theme in many papers at ICFP, and in the research of many</div><div>ICFP attendees, is the interaction of higher-order programming with</div><div>various kinds of effects: storage effects, I/O, control effects,</div>
<div>concurrency, etc. While effects are of critical importance in many</div><div>applications, they also make it hard to build, maintain, and reason</div><div>about one's code. Higher-order languages (both functional and</div>
<div>object-oriented) provide a variety of abstraction mechanisms to help</div><div>"tame" or "encapsulate" effects (e.g. monads, ADTs, ownership types,</div><div>typestate, first-class events, transactions, Hoare Type Theory,</div>
<div>session types, substructural and region-based type systems), and a</div><div>number of different semantic models and verification technologies have</div><div>been developed in order to codify and exploit the benefits of this</div>
<div>encapsulation (e.g. bisimulations, step-indexed Kripke logical</div><div>relations, higher-order separation logic, game semantics, various</div><div>modal logics). But there remain many open problems, and the field is</div>
<div>highly active.</div><div><br></div><div>The goal of the HOPE workshop is to bring researchers from a variety</div><div>of different backgrounds and perspectives together to exchange new and</div><div>exciting ideas concerning the design, semantics, implementation, and</div>
<div>verification of higher-order effectful programs.</div><div><br></div><div><br></div><div>---------------------</div><div>Workshop Organization</div><div>---------------------</div><div><br></div><div>Program Co-Chairs:</div>
<div><br></div><div>Derek Dreyer (MPI-SWS, Germany)</div><div>Hongseok Yang (University of Oxford)</div><div><br></div><div><br></div><div>Program Committee:</div><div><br></div><div>Anindya Banerjee (IMDEA Software Institute)</div>
<div>Lars Birkedal (Aarhus University)</div><div>Aquinas Hobor (National University of Singapore)</div><div>Chung-Kil Hur (Microsoft Research Cambridge)</div><div>Patricia Johann (Appalachian State University)</div><div>Matthew Might (University of Utah)</div>
<div>Peter Mueller (ETH Zurich)</div><div>Brigitte Pientka (McGill University)</div><div>Zhong Shao (Yale)</div><div><br></div></div>