I spoke at TEDx University of Ljubljana. The topic was how programming influences various aspects of life. I showed the audence how a bit of simple programming can reveal the beauty of mathematics. Taking John Baez’s The Bauty of Roots as an inspiration, I drew a very large image (20000 by 17500 pixels) of all roots of all polynomials of degree at most 26 whose coefficients are $-1$ or $1$. That’s 268.435.452 polynomials and 6.979.321.752 roots. It is two degrees more than Sam Derbyshire’s image, so consider the race to be on! Who can give me 30 degrees?
Here are the slides from my Logic Coloquium 2014 talk in Vienna. This is joint work with Kazuto Yoshimura from Japan Advanced Institute for Science and Technology.
Abstract: In constructive mathematics we often consider implications between non-constructive reasoning principles. For instance, it is well known that the Limited principle of omniscience implies that equality of real numbers is decidable. Most such reductions proceed by reducing an instance of the consequent to an instance of the antecedent. We may therefore define a notion of instance reducibility, which turns out to have a very rich structure. Even better, under Kleene’s function realizability interpretation instance reducibility corresponds to Weihrauch reducibility, while Kleene’s number realizability relates it to truth-table reducibility. We may also ask about a constructive treatment of other reducibilities in computability theory. I shall discuss how one can tackle Turing reducibility constructively via Kleene’s number realizability.
Slides with talk notes: lc2014-slides-notes.pdf
I just gave a talk at “Semantics of proofs and certified mathematics”. I spoke about a new proof checker Chris Stone and I are working on. The interesting feature is that it has both kinds of equality, the “paths” and the “strict” ones. It is based on a homotopy type system proposed by Vladimir Voevodsky. The slides contain talk notes and explain why it is “Brazilian”.
Abstract: Proof assistants verify that inputs are correct up to judgmental equality. Proofs are easier and smaller if equalities without computational content are verified by an oracle, because proof terms for these equations can be omitted. In order to keep judgmental equality decidable, though, typical proof assistants use a limited definition implemented by a fixed equivalence algorithm. While other equalities can be expressed using propositional identity types and explicit equality proofs and coercions, in some situations these create prohibitive levels of overhead in the proof.
Voevodsky has proposed a type theory with two identity types, one propositional and one judgmental. This lets us hypothesize new judgmental equalities for use during type checking, but generally renders the equational theory undecidable without help from the user.
Rather than reimpose the full overhead of term-level coercions for judgmental equality, we propose algebraic effect handlers as a general mechanism to provide local extensions to the proof assistant’s algorithms. As a special case, we retain a simple form of handlers even in the final proof terms, small proof-specific hints that extend the trusted verifier in sound ways.
On December 6th 2011 I gave a talk about homotopy equivalences in the context of homotopy type theory at our seminar for foundations of mathematics and theoretical computer science. I discuss the differences and relations between isomorphism (in the sense of type theory), an adjoint equivalence, and a homotopy equivalence. Even though the talk itself was not super-well prepared, I hope the recording will be interesting to some people. I was going fairly slowly, so it should be possible to follow the talk. I apologize for such a long video, but I really did not see how to chop it up into smaller pieces. Also, I need to figure out why I cannot fast forward the video beyond what has been downloaded.