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, provided 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 terms 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 of type theories.

The work presented in this talk has been done jointly with Philipp Haselwarter from the Faculty of Mathematics and Physics, University of Ljubljana.

Andrej Bauer is a professor of computational mathematics at the Faculty of Mathematics and Physics, University of Ljubljana. His research spans foundations of mathematics, constructive and computable mathematics, type theory, homotopy type theory, and principles of programming languages. With Matija Pretnar he designed the programming language Eff, the first language to support first-class algebraic effects and handlers. He was a member of the team of mathematicians who developed homotopy type theory at the Institute for Advanced Study. His latest research aims to provide a general mathematical understanding of what type theories are, and how we may implement them in practice, even when they lack good computational properties.