I was purging the disk on my laptop of large files and found a video lecture which I forgot to publish. Here it is with some delay. I lectured on how to implement type theory at the School and Workshop on Univalent Mathematics in December 2017, at the University of Birmingham (UK).
I have had the honor to lecture at the Oregon Programming Language Summer School 2018 on the topic of algebraic effects and handlers. The notes, materials and the lectures are available online:
- the GitHub repository with the course material
- the OPLSS lecture materials, including notes and video recordings of the lectures
I gave four lectures which started with the mathematics of algebraic theories, explained how they can be used to model computational effects, how we make a programming language out of them, and how to program with handlers.
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.
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].
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.