<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>------------</div><div>Registration </div><div>------------</div><div><br></div><div>Deadline for early registration: 22 August 2013 </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>
Special Session in Memory of John Reynolds</div><div>------------------------------------------</div><div><br></div><div>At this year's HOPE, we will organize a special session in memory of</div><div>the late John Reynolds, who developed several seminal results on the</div>
<div>design, semantics, and verification of higher-order programs with</div><div>effects. The session will include talks from the following invited</div><div>speakers:</div><div><br></div><div>Olivier Danvy</div><div>Robert Harper</div>
<div>Peter O'Hearn</div><div>Uday Reddy</div><div><br></div><div>This special session is sponsored in part by a generous donation</div><div>from Microsoft Research.</div><div><br></div><div>----------------------</div>
<div>List of Accepted Talks</div><div>----------------------</div><div><br></div><div>(1) Adam Chlipala. Adventures in Knot-Tying while Verifying a Thread Library in Coq</div><div><br></div><div>(2) Jeremy Siek. Linking isn't Substitution</div>
<div><br></div><div>(3) Danel Ahman. Refinement Types and Algebraic Effects</div><div><br></div><div>(4) Phillip Mates and Amal Ahmed. A Kripke Logical Relation for Affine Functions: The Story of a Free Theorem in the Presence of Non-termination</div>
<div><br></div><div>(5) Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey and German Andres Delbianco. Subjective Concurrent Protocol Logica</div><div><br></div><div>(6) Kasper Svendsen and Lars Birkedal. Impredicative Concurrent Abstract Predicates</div>
<div><br></div><div>(7) Armael Gueneau, Francois Pottier and Jonathan Protzenko. The ins and outs of iteration in Mezzo</div><div><br></div><div>(8) Andrzej Murawski and Nikos Tzevelekos. Deconstructing general references via game semantics</div>
<div><br></div><div>(9) Devin Coughlin and Bor-Yuh Evan Chang. Attacking the Imperative Relationship Update Problem with Almost Everywhere Heap Invariants</div><div><br></div><div>(10) David Swasey, Derek Dreyer, Deepak Garg and Robert Harper. Protocols for Protocols: Using Modal Separation Logic to Prove Extrinsic Properties of Secure Communication</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>