ICFP 2016

Full disclosure: This blog post is sponsored in part by ACM SIGPLAN. ACM SIGPLAN! Pushing the envelope of language abstractions for making programs better, faster, correcter, stronger.

TLDR

I went to ICFP again this year. I’m a frequent attendee. Last year I had a paper and gave a talk. This year I had a paper, but someone else gave the talk. But I also gave a talk at HOPE 2016. I met some people and saw some talks and pet a deer.

I’m a fifth year Ph.D. candidate studying compiler correctness, dependent types, and (functional) programming language abstractions. ICFP is my second home.

This year, I met some cool new researchers, several of whose names I’ve already forgotten (sorry new friends). I met Zoe Paraskevopoulou, who works on the CertiCoq project, a combination of my two favorite things: compiler correctness and dependent types. We talked a bit about this because I too have been looking at correctly compiling dependent types. I also met Éric Tanter, who works on, among many things, gradual typing and dependent types. He gave a talk on a method for verified interoperability with dependent types, which is related to certain kinds of compiler correctness problems that interest me, such as compositional compiler correctness and full abstraction. He’s also interested in Racket, so we spent some time discussing Cur.

I got some new ideas for Cur. David Christiansen’s talk on Elaborator Reflection: Extending Idris in Idris did a great job of motivating the problem and comparing meta-programming styles in proof assistants. The elaborator monad looks like a good abstraction for reasoning about certain kinds of extensions, and I need to figure out how to make it good for reasoning about the complex extensions possible in Cur. Jesper Cockx’s talk on Unifiers as Equivalences demonstrated ideas that might let me implement unification as a user defined extension in a proof-relevant way.

I saw most of the other talk, and a bunch of talks at the workshops. I have pages and pages of notes, and dozens of items in my TODO list to go and review papers and talks that I didn’t properly digest the first time. I hope I finish those by next year.