Posts in the category Andromeda
I gave a keynote talk "Derivations as Computations" at ICFP 2019.
- Slides with speaker notes: derivations-as-computations-icfp-2019.pdf
- Demo file: demo-icfp2019.m31
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.
- Slides: AndromedaProofAssistant.pdf
- Andromeda files: nat.m31, universe.m31