LFCS Seminar: 12 December 2018 - Jennifer Hackett

Title: How to Replace Sharing with Fortune-Telling

Abstract:

Lazy evaluation gives us two main benefits: compositional programming and infinite data. However, these benefits come at a cost, and one of the main reasons given in favour of strict (non-lazy) functional languages is that their operational behaviour is easier to understand. The key issue with understanding lazy evaluation is that while the external interface provided to the programmer is declarative and pure, the internal implementation is stateful. As a result, modelling lazy evaluation requires us to thread state through everything we do, vastly complicating our reasoning.

 In this talk, I will show how to avoid this problem by replacing the internal state of lazy evaluation with an external nondeterminism. This allows us to construct a much simplified semantics for lazy evaluation that still faithfully models concerns like efficiency. This talk is based on work currently in progress and is aimed at a broad audience of computer scientists, assuming a basic knowledge of operational semantics and the lambda calculus.

Bio: Jennifer Hackett is a post-doctoral researcher at the University of Nottingham working on the Mind the Gap project, developing techniques for reasoning about the efficiency of lazy functional programs. She also has an interest in computer creativity and human-computer collaboration, particularly for language-based art forms such as literature, poetry and interactive fiction. She is currently serving as Workshops Co-Chair for the International Conference on Functional Programming for the years 2019--2020, as well as on the programme committee for Mathematics of Program Construction 2019. In herspare time, she writes stories and songs with too many feelings in them.