ICFP 2012
The 17th ACM SIGPLAN International Conference on Functional Programming
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