The zipper is a useful data structure for navigating around tree-like structures in an efficient manner. I gave an introduction to the zipper, by starting with a simple type of trees
and then showing how to arrive at the following definitions:
Conor then explained the connection with differentiation, and also showed how to use the zipper to write an efficienct function that returns the mirror image of a tree. The lunch concluded with Nicolas Oury, who is visiting from France, explaining some of his work on simplifying the use of pattern matching in the Coq system.