A talk given at the University of Strathclyde in Glasgow, UK as part of the fun in the afternoon series of meetings. I describe current work with Dominic Mulligan on representing incompleteness in theorem-provers. Thanks to Conor McBride.
A talk given at the 16th meeting on Logic, Algebra, and Calculus at PPS in Paris, France. I talk about applications of nominal rewriting, algebra, and permissive-nominal logic to specifying and reasoning about logic, algebra, and calculus. Thanks to Delia Kesner and DIGITEO.