I have a keynote talk "Derivations as Computations" at ICFP 2019.
Abstract: According to the propositions-as-types reading, programs correspond to proofs, i.e., a term
t of type
A encodes a derivation
D whose conclusion is
t : A. But to be quite precise,
D may have parts which are not represented in
t, such as subderivations of judgmental equalities. In general, a term does not record an entire derivation, but only its proof relevant part. This is not a problem, as long as the missing subderivations can be reconstructed algorithmically. For instance, an equation may be re-checked, as long as we work in a type theory with decidable equality checking.
But what happens when a type theory misbehaves? For instance, the extensional type theory elides arbitrarily complex term through applications of the equality reflection principle. One may take the stance that good computational properties are paramount, and dismiss any type theory that lacks them – or one may look into the matter with an open mind.
If there is more to a derivation than its conclusion, then we should not equate the two. Instead, we can adopt a fresh perspective in which the conclusion is the result of a derivation. That is, we think of a derivation as a computation tree showing how to compute its conclusion. Moreover, the computation encoded by the derivation is effectful: proof irrelevance is the computational effect of discarding data, while checking a side condition is the effect of consulting an oracle. Where there are two computational effects, surely many others can be found.
Indeed, we may set up type theory so that any terminating computation represents a derivation, as long as the computational steps that construct type-theoretic judgments are guaranteed to be validated by corresponding inference rules. Common techniques found in proof assistants (implicit arguments, coercions, equality checking, etc.) become computational effects. If we allow the user to control the effects, say through the mechanism of Plotkin and Pretnar’s handlers for algebraic effects, we obtain a very flexible proof assistant capable of dealing with a variety type theories.
Here are the slides with speaker notes for the talk What is an explicit bijection which I gave at the 31st International Conference on Formal Power Series and Algebraic Combinatorics (FPSAC 2019). It was the "outsider" talk, where they invite someone to tell them something outside of their area.
So how does one sell homotopy type theory to people who are interested in combinatorics? That is a tough sell. I used my MathOverflow question "What is an explicit bijection?" to give a stand-up comedy introduction, after which I plunged into type theory. I am told I plunged a little too hard. For instance, people asked "why are we doing this" because I did not make it clear enough that we are trying to make a distinction between "abstractly exists" and "concretely constructed". Oh well, it’s difficult to explain homotopy type theory in 50 minutes. Anyhow, I hope you can get something useful from the slides.
Download slides: what-is-an-explicit-bijection.pdf
Video recording of the lecture is now available.
This semester my colleague Jaka Smrekar and I are teaching a graduate course on homotopy theory and homotopy type theory. The first part was taught by Jaka and was a nice review of classical homotopy theory leading up to Quillen model categories. In the second part I am covering basic homotopy type theory.
The course materials are available at the GitHub repository
homotopy-type-theory-course. The homotopy type theory lectures are also recorded on video.
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).
You may watch the video and visit the accompanying GitHub repository spartan-type-theory.
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:
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.
The slides from the talk “Spartan type theory”, given at the School and Workshop on Univalent Mathematics.
Download slides with speaker notes: Spartan Type Theory [PDF]
Here are the slides for the talk I just gave at TYPES 2017 in Budapest. It is joint work with Philipp Haselwarter and Théo Winterhalter. The abstract for the talk is available online.
It describes a complete formalization of dependent type theory which allows you to turn various features of type theory on and off, and it proves several basic formal theorems.
GitHub repository: formal-type-theory
Slides: TYPES 2017 – A modular formalization of type theory in Coq [PDF]
We are looking for two PhD students at the Faculty of Mathematics and Physics, University of Ljubljana. The programme starts in October 2017 and lasts three years. The positions will be fully funded (subject to approval by the funding agency). The candidates should have a Master’s degree in mathematics or computer science. No knowledge of Slovene is required.
The first PhD student will be advised by dr. Andrej Bauer. The topic of research is foundations of type theory. The candidate should have interest in mathematical aspects of type theory, and familiarity with proof assistants is desirable.
The second PhD student will be advised by dr. Matija Pretnar. The topic of research is the theory of programming languages with a focus on computational effects. The candidate should have interest in both the mathematical foundations and practical implementation of programming languages.
Candidates should send their applications as soon as possible, but no later than the end of April, to Andrej Bauer firstname.lastname@example.org or Matija Pretnar email@example.com, depending on their primary interest. Please include a short CV, academic record, and a statement of interest.
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)
It is my pleasure to announce the new and improved Programming languages Zoo, a potpourri of miniature but fully functioning programming language implementations. The new zoo has a decent web site, it is now hosted on GitHub, and the source code was cleaned up. Many thanks to Matija Pretnar for all the work.
The purpose of the zoo is to demonstrate design and implementation techniques, from dirty practical details to lofty theoretical considerations:
- functional, declarative, object-oriented, and procedural languages
- source code parsing with a parser generator
- recording of source code positions
- pretty-printing of values
- interactive shell (REPL) and non-interactive file processing
- untyped, statically and dynamically typed languages
- type checking and type inference
- subtyping, parametric polymorphism, and other kinds of type systems
- eager and lazy evaluation strategies
- recursive definitions
- interpreters and compilers
- abstract machine
There is still a lot of room for improvement and new languages. Contributions are welcome!