Abstract

Addition and multiplication of types can be defined by the union and cartesian product operations. Can we go further? We try out exponentiation, limits, differentiation and even subtraction of types. Along the way we run into such oddities as the type of all binary trees is isomorphic to the type of all seven-tuples of binary trees, and that a bag with a hole in it is still a bag.

About the Speaker

I received a PhD in geophysics from MIT, masters in number theory from Universita degli Studi di Milano, and BS in mathematics from Caltech. I participated in the ICPC world finals in 2006 and 2011 and coached the Caltech teams in 2007 and 2009, including a bronze medal.