14th November

How to be a Productive Programmer

On Friday, I gave a talk at the Scottish Programming Languages Seminar (SPLS) at Heriot-Watt. Many thanks to Greg Michaelson for organising everything and giving me time to speak.

I've put the slides I used on-line as a PDF file (with two small fixes, see below).

The talk presents an extension of a Nakano-style typed λ-calculus with a delay modality for guarded recursion. In short, this means:

As I mentioned during the talk, this is based on Conor's blog post Time files like an Applicative Functor from over two years ago.

The hoped-for outcome is a nice way of programming with codata in a functional language like Haskell. Still more hopefully, this will extend to systems with dependently types too, though I am still confused about where the clock variables ought to live.

I fixed two typos that were present in copy of the slides that I used in the talk: