Mathematics and Computation

A blog about mathematics for computers

Postsby categoryby yearall

Posts in the category Andromeda

I gave a keynote talk "Derivations as Computations" at ICFP 2019.

continue reading

What is a formal proof?

Mike Shulman just wrote a very nice blog post on what is a formal proof. I much agree with what he says, but I would like to offer my own perspective. I started writing it as a comment to Mike's post and then realized that it is too long, and that I would like to have it recorded independently as well. Please read Mike's blog post first.

continue reading (55 comments)

I am about to give an invited talk at the  Workshop on Categorical Logic and Univalent Foundations 2016 in Leeds, UK. It's a charming workshop that I am enjoing a great deal. Here are the slides of my talk, with speaker notes, as well as the Andromeda examples that I am planning to cover.

continue reading (30 comments)
Postsby categoryby yearall