Day 1

Day 2

09:00 Invited talk: Programming Assurance Cases in Agda
Makoto Takeyama
10:00 Break
10:30 On the Bright Side of Type Classes: Instance Arguments in Agda
Dominique Devriese and Frank Piessens (K.U.Leuven)
10:55 Experience Report: Functional Modelling of Musical Harmony
José Pedro Magalhães and W. Bas de Haas (Utrecht University)
11:15 How to Make Ad Hoc Proof Automation Less Ad Hoc
Georges Gonthier (Microsoft Research), Beta Ziliani (MPI-SWS), Aleksandar Nanevski (IMDEA Software Institute), and Derek Dreyer (MPI-SWS)
11:40 Lunch
13:10 Temporal Higher-Order Contracts
Tim Disney and Cormac Flanagan (University of California, Santa Cruz) and Jay McCarthy (Brigham Young University)
13:35 Functional Pearl: Parsing with Derivatives
Matthew Might and David Darais (University of Utah) and Daniel Spiewak (University of Wisconsin-Milwaukee)
13:45 An Efficient Non-Moving Garbage Collector for Functional Languages
Katsuhiro Ueno, Atsushi Ohori, and Toshiaki Otomo (Tohoku University)
14:10 Break
14:40 Deriving an Efficient FPGA Implementation of a Low Density Parity Check Forward Error Corrector
Andy Gill and Andrew Farmer (University of Kansas)
15:05 Geometry of Synthesis IV
Dan R. Ghica and Alex Smith (University of Birmingham) and Satnam Singh (Microsoft Research)
15:30 Break
16:00 The Mendler Hierarchy of Recursion Combinators: Taming Inductive Datatypes with Negative Occurrences.
Ki Yung Ahn and Tim Sheard (Portland State University)
16:25 Typed Self-Interpretation by Pattern Matching
C. Barry Jay (University of Technology, Sydney) and Jens Palsberg (UCLA, University of California, Los Angeles)
16:50 Experience report: Using Camlp4 for Presenting Dynamic Mathematics on the Web: DynaMoW, an OCaml language extension for the run-time generation of mathematical contents and their presentation on the Web
Frederic Chyzak (INRIA) and Alexis Darrasse (Universite Paris 6)
17:10 Break
17:30 Announcement of ICFP'12
17:40 Most Influential ICFP'01 Paper Award
17:50 SIGPLAN Software Award
18:00 Report on the Fourteenth ICFP Programming Contest
19:45 Conference Banquet (Meguro Gajoen)

Day 3

09:00 Secure Distributed Programming with Value-Dependent Types
Nikhil Swamy, Juan Chen, and Cedric Fournet (Microsoft Research), Pierre-Yves Strub (MSR-INRIA), Karthikeyan Bhargavan (INRIA), and Jean Yang (MIT)
09:25 Frenetic: A Network Programming Language
Nate Foster (Cornell University), Rob Harrison, Michael J. Freedman, Christopher Monsanto, and Jennifer Rexford (Princeton University), Alec Story (Cornell University), and David Walker (Princeton University)
09:50 Break
10:20 Forest: A Language and Toolkit For Programming with Filestores
Kathleen Fisher (Tufts University), Nate Foster (Cornell University), David Walker (Princeton University), and Kenny Q. Zhu (Shanghai Jiao Tong University)
10:45 Making Standard ML a Practical Database Programming Language
Atsushi Ohori and Katsuhiro Ueno (Tohoku University)
11:10 Break
11:40 Nameless, Painless
Nicolas Pouillard (INRIA)
12:05 Binders Unbound
Stephanie Weirich and Brent Yorgey (University of Pennsylvania) and Tim Sheard (Portland State University)
12:30 Recursion principles for syntax with bindings and substitution
Andrei Popescu (Technical University Munich) and Elsa Gunter (University of Illinois)
12:55 Lunch
14:25 Proving The Unique Fixed-Point Principle Correct - An Adventure with Category Theory
Ralf Hinze and Daniel W. H. James (University of Oxford)
14:50 Linearity and PCF: a semantic insight!
Marco Gaboardi (Universita di Bologna), Luca Paolini (Universita di Torino), and Mauro Piccolo (Politecnico di Torino)
15:15 Break
15:45 Generalising and Dualising the Third List-Homomorphism Theorem
Shin-Cheng Mu (Academia Sinica, Taiwan) and Akimasa Morihata (Tohoku University, Japan)
16:10 Incremental Updates for Efficient Bidirectional Transformations
Meng Wang (Chalmers University of Technology) and Jeremy Gibbons and Nicolas Wu (University of Oxford)
16:35 Break
17:05 Modular verification of preemptive OS kernels
Alexey Gotsman (IMDEA Software Institute) and Hongseok Yang (Queen Mary University of London)
17:30 Characteristic Formulae for the Verification of Imperative Programs
Arthur Chargueraud (Max-Planck Institute for Software Systems)
17:55 Break
18:15 An Equivalence-Preserving CPS Translation via Multi-Language Semantics
Amal Ahmed (Indiana University) and Matthias Blume (Google)
18:40 A Kripke Logical Relation for Effect-Based Program Transformations
Jacob Thamsborg and Lars Birkedal (IT University of Copenhagen)
19:05 Closure