Abstract:

Infinite objects in programs, such as streams, are usually constructed via self-referential definitions.  Such definitions, however, are easy to get wrong.  How can a programming language be designed to permit 'good' self-references while disallowing the nonsensically circular ones?  And how could we reason about the correctness of programs written in such a language?

Rather surprisingly, an old logic from the 1950s, Gödel-Löb provability logic, suggests a solution.  This logic provides a method both to define infinite objects via 'good' self-references, and to reason about them.  This method is called 'guarded recursion' and employs a type-former called 'later' that allows us to control when self-references are called upon.

Short bio:

Ranald Clouston began his studies at Victoria University of Wellington in New Zealand, then took a PhD at the University of Cambridge, graduating in 2010.  He then held a postdoctoral position with the Logic and Computation group at Australian National University, and currently works as a postdoc in the Logic and Semantics group at Aarhus University.  His research interests include type theory, separation logic, linear logic, coalgebra, and nominal logic.