Copenhagen, Denmark
September 10 – 12, 2012

September 10

8:45 Welcome
9:00 Keynote: Conor McBride
Agda-curious?: An Exploration of Programming with Dependent Types
10:00 Break
10:20 Automated Theorem Proving (Chair: Stephanie Weirich)
Verified Heap Theorem Prover by Paramodulation
Gordon Stewart, Lennart Beringer, and Andrew W. Appel (Princeton University)
Formal Verification of Monad Transformers
Brian Huffman (T.U. Munich)
11:00 Break
11:20 Types (Chair: Lars Birkedal)
Elaborating Intersection and Union Types
Joshua Dunfield (MPI-SWS)
An Error-Tolerant Type System for Variational Lambda Calculus
Sheng Chen, Martin Erwig, and Eric Walkingshaw (Oregon State University)
Superficially Substructural Types
Neelakantan R. Krishnaswami (MPI-SWS), Aaron Turon (Northeastern University), and Derek Dreyer and Deepak Garg (MPI-SWS)
12:20 Lunch/Posters
14:00 Business Meeting – PC Chair's slides
14:40 Break
15:00 Embedded Languages (Chair: Sam Tobin-Hochstadt)
Shake Before Building - Replacing Make with Haskell
Neil Mitchell
Practical Typed Lazy Contracts
Olaf Chitil (University of Kent)
15:40 Break
16:00 Programming with Graphs and Search (Chair: Jeremy Gibbons)
Functional Programming with Structured Graphs
Bruno Oliveira (Seoul National University) and William R. Cook (University of Texas, Austin)
Painless programming combining reduction and search. Design principles for embedding decision procedures in high-level languages.
Tim Sheard (Portland State University)
16:40 Break
17:00 Ornaments, Extraction, and Semantics (Chair: John Hughes)
Transporting Functions across Ornaments
Pierre-Evariste Dagand and Conor McBride (MSP group, University of Strathclyde)
Proof-Producing Synthesis of ML from Higher-Order Logic
Magnus O. Myreen and Scott Owens (University of Cambridge)
Operational Semantics Using the Partiality Monad
Nils Anders Danielsson (Chalmers University of Technology and University of Gothenburg)

September 11

9:00 Keynote: Kunle Olukotun
High Performance Embedded Domain Specific Languages
10:00 Break
10:20 Infinity (Chair: Graham Hutton)
Pure Type Systems with Corecursion on Streams
Paula Severi and Fer-Jan de Vries (University of Leicester)
On the Complexity of Equivalence of Specifications of Infinite Objects
Jörg Endrullis, Dimitri Hendriks, and Rena Bakhshi (VU University Amsterdam)
11:00 Break
11:20 Compilers (Chair: Andreas Rossberg)
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)
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)
12:00 Lunch/Posters
14:00 Contest Report
14:40 Break
15:00 Security (Chair: Eijiro Sumii)
Efficient Lookup-Table Protocol in Secure Multiparty Computation
John Launchbury, Andy Adams-Moran, and Iavor Diatchki (Galois, Inc.)
Addressing Covert Termination and Timing Channels in Concurrent Information Flow Systems
Deian Stefan (Stanford University), Alejandro Russo and Pablo Buiras (Chalmers University), and Amit Levy, John C. Mitchell, and David Mazieres (Stanford University)
15:40 Break
16:00 FP in Biology (Chair: Zhenjiang Hu)
Sneaking Around concatMap -- Efficient Combinators for Dynamic Programming
Christian Höner zu Siederdissen (University of Vienna, Vienna, Austria)
Experience Report: Haskell in Computational Biology
Noah M. Daniels, Andrew Gallant, and Norman Ramsey (Tufts University)
16:40 Break
17:00 Parallelism (Chair: Simon Marlow)
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)
Nested Data-Parallelism on the GPU
Lars Bergstrom and John Reppy (University of Chicago)
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)

September 12

9:00 Keynote: Peter Sewell
Tales from the Jungle
10:00 Break
10:20 Curry-Howard and Compatibility Checking (Chair: Amal Ahmed)
Propositions as Sessions
Philip Wadler (University of Edinburgh)
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)
11:00 Break
11:20 DSL Support (Chair: Satnam Singh)
Deconstraining DSLs
Will Jones, Tony Field, and Tristan Allwood (Department of Computing, Imperial College London)
Explicitly Heterogeneous Metaprogramming with MetaHaskell
Geoffrey Mainland (Microsoft Research)
A generic abstract syntax model for embedded languages
Emil Axelsson (Chalmers University of Technology)
12:20 Lunch
14:00 SRC Poster Presentations
15:40 Break
16:00 Analysis (Chair: Peter Thiemann)
Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs
Hugo Simões, Pedro Vasconcelos, and Mário Florido (Universidade do Porto), Steffen Jost (Ludwig-Maximilians-Universität Munich), and Kevin Hammond (University of St Andrews)
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)
16:40 Break
17:00 Higher-order Model Checking and Slicing (Chair: Colin Runciman)
A Traversal-based Algorithm for Higher-Order Model Checking
Robin P. Neatherway, C.-H. Luke Ong, and Steven J. Ramsay (University of Oxford)
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)
17:40 Closing