Copenhagen, Denmark
September 9 – 15, 2012

Elaborating Intersection and Union Types
Joshua Dunfield (MPI-SWS)
A Meta-Scheduler for the Par-Monad: Composable Scheduling for the Heterogeneous Cloud
Adam Foltzer, Abhishek Kulkarni, Rebecca Swords, Sajith Sasidharan, Eric Jiang, and Ryan R. Newton (Indiana University)
Shake Before Building - Replacing Make with Haskell
Neil Mitchell
Experience Report: a Do-It-Yourself High-Assurance Compiler
Lee Pike (Galois, Inc.), Nis Wegmann (University of Copenhagen), Sebastian Niller (Unaffiliated), and Alwyn Goodloe (NASA)
Transporting Functions across Ornaments
Pierre-Evariste Dagand and Conor McBride (MSP group, University of Strathclyde)
Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs
Pedro Vasconcelos, Hugo Simoes, and Mario Florido (Universidade do Porto), Steffen Jost (Ludwig-Maximilians-Universitat Munich), and Kevin Hammond (University of St Andrews)
Verified Heap Theorem Prover by Paramodulation
Gordon Stewart, Lennart Beringer, and Andrew W. Appel (Princeton University)
Pure Type Systems with Corecursion on Streams
Paula Severi and Fer-Jan de Vries (University of Leicester)
A Traversal-based Algorithm for Higher-Order Model Checking
Robin P. Neatherway, C.-H. Luke Ong, and Steven J. Ramsay (University of Oxford)
Experience Report: Haskell in Computational Biology
Noah M. Daniels, Andrew Gallant, and Norman Ramsey (Tufts University)
Functional Programming with Structured Graphs
Bruno Oliveira (Seoul National University) and William R. Cook (University of Texas, Austin)
Nested Data-Parallelism on the GPU
Lars Bergstrom and John Reppy (University of Chicago)
Deconstraining DSLs
Will Jones, Tony Field, and Tristan Allwood (Department of Computing, Imperial College London)
Formal Verification of Monad Transformers
Brian Huffman (T.U. Munich)
MetaHaskell: Type Safe Heterogeneous Metaprogramming
Geoffrey Mainland (Microsoft Research)
Introspective Pushdown Analysis of Higher-order Programs
Christopher Earl (University of Utah), Ilya Sergey (KU Leuven), Matthew Might (University of Utah), and David Van Horn (Northeastern University)
On the Complexity of Equivalence of Specifications of Infinite Objects
Jörg Endrullis, Dimitri Hendriks, and Rena Bakhshi (VU University Amsterdam)
Efficient Lookup-Table Protocol in Secure Multiparty Computation
John Launchbury, Andy Adams-Moran, and Iavor Diatchki (Galois, Inc.)
Proof-Producing Synthesis of ML from Higher-Order Logic
Magnus O. Myreen and Scott Owens (University of Cambridge)
Propositions as Sessions
Philip Wadler (University of Edinburgh)
Work Efficient Higher Order Vectorisation
Ben Lippmeier, Manuel M. T. Chakravarty, Gabriele Keller, and Roman Leshchinskiy (University of New South Wales) and Simon Peyton Jones (Microsoft Research Ltd)
A generic abstract syntax model for embedded languages
Emil Axelsson (Chalmers University of Technology)
Equality proofs and deferred type errors (A compiler pearl)
Dimitrios Vytiniotis and Simon Peyton Jones (Microsoft Research Cambridge) and José Pedro Magalhães (Utrecht University)
Painless programming combining reduction and search. Design principles for embedding decision procedures in high-level languages.
Tim Sheard (Portland State University)
An Error-Tolerant Type System for Variational Lambda Calculus
Sheng Chen, Martin Erwig, and Eric Walkingshaw (Oregon State University)
Practical Typed Lazy Contracts
Olaf Chitil (University of Kent)
Superficially Substructural Types
Neelakantan R. Krishnaswami (MPI-SWS), Aaron Turon (Northeastern University), and Derek Dreyer and Deepak Garg (MPI-SWS)
Functional Programs that Explain their Work
Roly Perera and Umut A. Acar (Max Planck Institute for Software Systems), James Cheney (University of Edinburgh), and Paul Blain Levy (University of Birmingham)
Operational Semantics Using the Partiality Monad
Nils Anders Danielsson (Chalmers University of Technology and University of Gothenburg)
Typing unmarshalling without marshalling types
Grégoire Henry (Univ Paris Diderot), Michel Mauny (ENSTA-ParisTech), and Emmanuel Chailloux and Pascal Manoury (Université Pierre et Marie Curie)
Addressing Covert Termination and Timing Channels in Concurrent Information Flow Systems
Deian Stefan (Stanford University), Alejandro Russo (Chalmers University), Pablo Buiras (Chalmers University), Amit Levy (Stanford University), John C. Mitchell (Stanford University), David Mazieres (Stanford University)