In 2013 I gave a talk about constructive mathematics “Five stages of accepting constructive mathematics” (video) at the Institute for Advanced Study. I turned the talk into a paper, polished it up a bit, added things here and there, and finally it has now been published in the Bulletin of the American Mathematical Society. It is not quite a survey paper, but it is not very technical either. I hope you will enjoy reading it.
Free access to the paper: Five stages of accepting constructive mathematics (PDF)
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?
Here are the slides of my TYPES 2015 talk “The troublesome reflection rule” with fairly detailed presenter notes. The meeting is taking place in Tallinn, Estonia – a very cool country in many senses (it’s not quite spring yet even though we’re in the second half of May, and it’s the country that gave us Skype).
Download slides: The troublesome reflection rule (TYPES 2015) [PDF].
This is a draft version of my contribution to “A Computable Universe: Understanding and Exploring Nature as Computation”, edited by Hector Zenil. Consider it a teaser for the rest of the book, which contains papers by an impressive list of authors.
Abstract: Intuitionistic mathematics perceives subtle variations in meaning where classical mathematics asserts equivalence, and permits geometrically and computationally motivated axioms that classical mathematics prohibits. It is therefore well-suited as a logical foundation on which questions about computability in the real world are studied. The realizability interpretation explains the computational content of intuitionistic mathematics, and relates it to classical models of computation, as well as to more speculative ones that push the laws of physics to their limits. Through the realizability interpretation Brouwerian continuity principles and Markovian computability axioms become statements about the computational nature of the physical world.
The HoTT book is finished!
Since spring, and even before that, I have participated in a great collaborative effort on writing a book on Homotopy Type Theory. It is finally finished and ready for public consumption. You can get the book freely at http://homotopytypetheory.org/book/. Mike Shulman has written about the contents of the book, so I am not going to repeat that here. Instead, I would like to comment on the socio-technological aspects of making the book, and in particular about what we learned from open-source community about collaborative research.
Continue reading The HoTT book