Today I just got back from the lovely Melbourne, where I was attending both the Asian Symposium on Programming Languages and Systems (APLAS) and Certified Programs and Proofs (CPP), two small conferences that were colocated this year. More information are available on the APLAS2013 and CPP2013 websites.

There were a number of standout talks, and I summarise here just the ones that I remember most prominently:

APLAS

• Alexandra Silva presented some fascinating work on the common (co)-algebraic structure of various kinds of automata, and a naturally generic version of Brzozowski’s algorithm defined on top of it.

• Sukyeong Ryu presented a modest extension of Java with so-called “exact” types, which solve an aspect of type expression that is cumbersome in typical object-oriented setting but easy in something like static type-classes.

• Jacques Gerrigue presented his work on type inference for GADTs in OCaml. Notably it avoids the complicated constraint systems of GHC’s OutsideIn(X), instead using so-called ambivalent types to track and confine ambiguity in type reconstruction.

• Fritz Henglein presented a beautifully simple piece of code, a domain specific language for expressing orders, and showed how it can be used to create highly efficient radix sorts and tries.

• Matthias Puech showed that the correspondence between natural deduction and sequent calculus is, via formulae-as-types, exactly the same transformation that functional programmers make all the time when saving stack-space: rewriting a function to be tail recursive by adding accumulators.

CPP

• Nick Benton presented his work embedding a large amount of assembly language within Coq, combining it with a machine model and using it for verification.

• Denis Firsov presented a nice theory of regular languages in Agda, expressing automata transitions as matrices and regular language operations as matrix operations. This enables a kind of algebraic reasoning about automata that makes certified parsing proofs straightforward and elegant.

• Dan Licata gave an introduction to Homotopy Type Theory and higher inductive types, which was fascinating and also good at giving us all a status update on the progress of the entire univalent foundations programme.

• Ondřej Kunčar presented some much-desired Isabelle extensions for lifting and transfer on quotient types.

• Carroll Morgan gave a captivating talk on his and others work on noninterference security for probabilistic systems.

Of course, there were many other talks that had interesting and varied contributions, but these were the talks that I found personally enjoyable to listen to and interesting enough to note down. Many thanks go to the organisers, and to Chung-chieh Shan who asked many of the questions we all wanted to ask.