PPDP 2014

PPDP 2014

I attended PPDP 2014, in Canterbury, England a few weeks ago.  Some notes about papers of interest there:


Read more »

SIGMOD 2014

I totally failed to post a trip report on POPL 2014, and I'm now attending SIGMOD/PODS 2014, in Snowbird, Utah, so I'm writing the post during the conference to ensure I don't forget later.  This is the first time I've been to SIGMOD in a while.  There are usually 4-5 parallel tracks so it is impossible to see more than a fraction of the talks, but fortunately the talks I was most interested in were usually in separate sessions, so there were only a few tough decisions.  There were many good talks, but several stood out:
Read more »

Nominal Sets and Nominal Computation Theory

Nominal Sets: Names and Symmetry in Computer Science
Andrew M. Pitts
Cambridge, 2013 (see also recent lecture notes)

Dagstuhl Seminar on Nominal Computation Theory
(organized by Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, and Andrew M. Pitts)

$\newcommand{\AA}{\mathbb{A}}$Part of my summer reading was Pitts' recent book on nominal sets.  Let $\AA$ be a set of names. A nominal set is a set $X$ equipped with a permutation action, that is, a function $\cdot_X :  Perm(\AA) \times X \to X$ where $Perm(\AA)$ is the set of all (finite) permutations on $X$.  Being a permutation action means that $id\cdot_X x = x$ and $(\pi \circ \pi') \cdot_X x = \pi \cdot_X \pi' \cdot_X x$ for all $\pi,\pi' \in Perm(\AA)$.  In addition, a nominal set must satisfy a finite-support property, which (oversimplifying slightly) requires that for each element there is a least support set $supp(x) \subseteq \AA$ such that for all $a,b \notin supp(x)$ we have $(a~b)\cdot_X x = x$.  Intuitively, the support is the set of names "appearing in" $x$, though in general there is no requirement that $X$ be a set of abstract syntax trees in the usual sense.


Read more »

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.
Read more »

LFMTP 2013 and logical frameworks

8th International Workshop on Logical Frameworks and Meta-Langauges: Theory and Practice (LFMTP 2013)

Robert Harper, Furio Honsell, and Gordon Plotkin. 1993. A framework for defining logics. J. ACM 40, 1 (January 1993), 143-184.

I'm gratuitously attending ICFP 2013 (i.e., I'm not presenting or helping organize, though I was on the LFMTP PC).

This year's LFMTP celebrated the 20th anniversary of the publication of Harper, Honsell and Plotkin's "A framework for defining logics".  I want to say a few words about that work and draw a line connecting it to currently exciting activities in the functional PL world, many of which were presented yesterday at ICFP.

Harper, Honsell and Plotkin introduced LF, which is a dependent type theory (essentially the same as what is often also called $\lambda$P, one of the corners of the lambda cube).  Expressions are classified into kinds, types, and objects; kinds classify types; types classify objects.  Types can depend on objects and kinds on types.

Read more »

DBPL 2013

DBPL 2013

I attended DBPL 2013 in Riva Del Garda, Italy - a very attractive venue.  I was stupid and only came for the day of the workshop.  There were a lot of interesting talks.
Read more »