[This post is by Harley Eades III. AS]
I just returned from the 2010 ACM SIGNPLAN International Conference on Functional Programming and the Haskell Symposium held in Baltimore, Maryland. I would like to share my thoughts on which talks I found to be the most interesting this year. The first talk was by Mike Gordon titled, “ML: Metalanguage or Object Language”. The subject of this wonderfully put together talk was about the life of Robin Miller, who recently passed away. I found this to be a very interesting talk especially regarding Robin Miller’s research on Edinburgh LF and ML.
The second talk was “Higher-order Representation of Substructural Logics” by Karl Crary. In his paper he presents a technique for a higher-order representation of substructural logics such as linear logic and modal logic. He goes on to show that there is an encoding of these representations into Logical Framework (LF) without adding any extensions to LF. This is pretty cool stuff, because it allows one to reason about linear and modal logics in proof assistants based on LF. His work makes me wonder if there exists encodings into other frameworks allowing one to use other proof assistants not based on LF.
The third talk I would like to comment on was titled, “Species, Functors, and Types, Oh My!” by Brent A. Yorgey. I have to say that Brent’s talk stole the show. Between all of the talks at ICFP and the symposium this was by far the most entertaining talk. He started his talk by pretending to be a prophet sent by the gods of combinatorics. He was able to move from a series of great jokes into very interesting research. His talk/paper introduces the use of a pure mathematical theory called combinatorial species which can be used as a language for talking about algebraic data types. I am still going though his paper, but I think it may be a very useful tool. All in all ICFP and the Haskell Symposium was great. I look forward to diving into the proceedings and really getting into the details of everyones work.