ICFP 2013

ICFP 2013 (The 18th ACM SIGPLAN International Conference on Functional Programming)

ICFP is the conference I attend most regularly; since 2002 I've attended every year except 2004, 2007 and 2011.  As mentioned in the last post, I attended ICFP 2013 in Boston, somewhat gratuitously: I wasn't presenting our paper, but was excited by the program and wanted to see a lot of talks. I wasn't disappointed.  I attended just about every session.  Here is a quick summary of papers/talks that especially stood out, with some reactions:  (Please don't be offended if I don't mention your paper - all the talks were good, but these were the ones that made a special impression)

Day 1:

The first day had a distinctively dependently-typed feel, with a little algorithms thrown in.

• Ulf Norell, Interactive Programming with Dependent Types.  The talk was basically a walkthrough of a nontrivial programming exercise in Agda: program a typechecker for simply-typed lambda terms, making elegant use of Agda's code completion facilities to construct either a proof of well-formedness or a proof of ill-formedness.  Thinking carefully about how to design the type of "proofs of P or not P" gives the typechecker/proof search engine what it needs to write lots of boilerplate code for you.  There are interesting connections to negation elimination, I think...
• Optimising Purely Functional GPU Programs, Trevor L. McDonell, Manuel Chakravarty, Gabriele Keller and Ben Lippmeier. Fits into the emerging story I've been seeing of carving out subsets of (purely) functional languages that can be compiled and optimized efficiently on high-performance systems.  I'll definitely be reading this paper.
• Type-Theory In Color, Jean-Philippe Bernardy and Guilhem Moulin.  I'd heard a lot about this paper but unfortunately wound up missing the beginning of the talk and sitting too far back to appreciate the talk.  Need to read the paper.
• Functional Geometry and the "Traité de Lutherie" [Functional Pearl], Harry Mairson. This pearl/talk was about using functional languages to define geometric constructions like those used in the Middle Ages/Renaissance to construct musical instruments.  This talk was one of the highlights of the conference, and the paper looks enjoyable to read also. 
• Fun with Semirings [Functional Pearl], Stephen Dolan.  A nice exploration of semiring-based algorithms.  I think a lot of this is folklore to the algorithms community (especially people like Dexter Kozen) but it is nice to see it presented accessibly to the FP community.
• Programming and Reasoning with Algebraic Effects and Dependent Types, Edwin Brady; Handlers in Action, Ohad Kammar, Sam Lindley and Nicolas Oury.  Two interesting takes on embedding algebraic effects and handlers in functional languages, using dependent types and Haskell-style GADT/classes/metaprogramming respectively.  I've read earlier drafts of Handlers in Action and plan to read Edwin's paper too.

Day 2:  

There were a number of talks exploring variations on the theme of coinduction, functional reactive and stream programming.

• Computer Science as a School Subject, Simon Peyton Jones.  This talk was an overview of the Computing at School effort, which aims to replace the (skills-focused) "Information and Communication Technology" curriculum in UK primary and secondary education with a new curriculum that emphasizes fundamental concepts such as algorithms. 
• Programming with Permissions in Mezzo, Francois Pottier and Jonathan Protzenko.  A very interesting language design paper, basically about combining separation logic ideas with types to allow for efficient implementations of monotonically mutable functional data structures. Also going on my reading list.
• Wellfounded Recursion with Copatterns, Andreas Abel and Brigitte Pientka.
  The first looks at defining stream-like (or other coinductive) values via patterns that say how the stream responds to various operations.
• Productive Coprogramming with Guarded Recursion, Robert Atkey and Conor McBride.  Another proposal for ensuring productivity for coinductive types; uses a modal "tomorrow" type to ensure productivity.  
• Higher-Order Functional Reactive Programming without Spacetime Leaks, Neelakantan Krishnaswami.  Also a paper/talk I'm somewhat familiar with, but will have to take a closer look.  Similar to Atkey and McBride, uses a modal / temporal logic-inspired box type to avoid writing programs that "preserve too much history".
• Using Circular Programs for Higher-Order Syntax [Functional Pearl], Emil Axelsson and Koen Claessen.  A very nice observation that one can use lazily-infinite values to avoid explicit fresh-name generation.  It would be interesting to compare this with Randy Pollack and others' recent approach.

Day 3:

Day 3 had a number of talks looking at different applications or techniques for modularizing/encapsulating language features and reasoning about languages.  For me, there were fewer memorable talks, though this may more be because of tiredness than anything to do with the speakers or material.  There were also pairs of talks that seemed to cover similar ground, and I'm typically only summarizing one of them below.

• The Constrained-Monad Problem, Neil Sculthorpe, Jan Bracker, George Giorgidze and Andy Gill.  What do you do if your monadic operations need a class constraint?  Then they don't form a (Haskell) monad, which is a pain.  This paper works out how to fix this by adding an appropriate layer of indirection.  
• Modular Monadic Meta-Theory, Benjamin Delaware, Steven Keuchel, Tom Schrijvers and Bruno Oliveira.  What if you have a mechanized type safety proof for a language with references, and another proof for a language with exceptions, and you want to combine them to prove type safety for references AND exceptions?  It's a pain.  This paper gives a way to make the proofs modular so that they can be freely combined.  (But what about polymorphism, you may well ask...)
• Functional Programming of mHealth Applications [Experience Report], Christian Petersen, Matthias Gorges, Dustin Dunsmuir, Mark Ansermino and Guy Dumont.  Currently mobile health apps are written in languages like Matlab or R.  Hard to maintain and trust.  The authors are doing this using Scheme.  Take home message: Functional programming to save people's lives.  Definitely another highlight of the conference.
• Optimizing Abstract Abstract Machines, J. Ian Johnson, Nicholas Labich, Matthew Might and David Van Horn.  Shows how to take the (elegant, but inefficient) "Abstracting Abstract Machines" approach to static analysis and make it practical - not quite yet equivalent to hand-coded techniques, but several order of magnitudes better. 

Stray thoughts:

• Apparently ICFP had over 370 people registered this year, and 500 attendees total including workshops.  That's a lot.  I remember when it was a big deal that registration passed 200.
• The conference hotel (Hilton, Boston Logan Airport) was a little remote when it comes to doing something in the evening, but it grew on me - it did at least mean people had nowhere else to go during the day.
• Phil's talk featured the brightest laser pointer I've ever seen.  (I'll link to the video when it's available...)