Andrej Bauer: Derivations as computations

Abstract: An inference rule in type theory, or generally in a formal system, is a syntactic form which requires an interpretation.  A standard reading of inference rules is that they are the closure conditions, or inductive constructors, which generate derivations.  Therefore derivations are well-founded trees, freely generated by the inference rules.

I will entertain the possibility that derivations need not be freely generated by the rules.  The basis for such a speculation is the observation that derivation trees represent processes for establishing judgments, but are not the processes themselves.  Indeed, a mathematician's mind most certainly does not contain derivation trees, but instead arrives at a conclusion through a mental process that can be viewed as traversal of a derivation tree.  Similarly, a derivation in a proof assistant exists only implicitly in the execution trace of the program.

Once we allow inference rules to be interpreted as general operations, rather than data constructors, appealing possibilities arise.  For instance, an inference rule can be read as a proof transformation, or as a computation which may have a side-effect, one of which is proof irrelevance.  When these ideas are pushed into practice, they motivate the design of a proof assistant in which inference rules correspond to algebraic operations whose interpretation can be specified by the user.

[The halftime break may be extended if audience members want to attend Jesper Carlström’s talk “Formella metoder för järnväg”, 10:45–11:15.]