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.
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.
I am about to give an invited talk at the Computability and Complexity in Analysis 2016 conference (yes, I am in the south of Portugal, surrounded by loud English tourists, but we are working here, in a basement no less). Here are the slides, with extensive speaker notes, comment and questions are welcome.
In a paper accepted at POPL 2016 Matt Brown and Jens Palsberg constructed a self-interpreter for System $F_\omega$, a strongly normalizing typed $\lambda$-calculus. This came as a bit of a surprise as it is “common knowledge” that total programming languages do not have self-interpreters.
Thinking about what they did I realized that their conditions allow a self-interpreter for practically any total language expressive enough to encode numbers and pairs. In the PDF note accompanying this post I give such a self-interpreter for Gödel’s System T, the weakest such calculus. It is clear from the construction that I abused the definition given by Brown and Palsberg. Their self-interpreter has good structural properties which mine obviously lacks. So what we really need is a better definition of self-interpreters, one that captures the desired structural properties. Frank Pfenning and Peter Lee called such properties reflexivity, but only at an informal level. Can someone suggest a good definition?