MF#K: An introduction to Martin-Löf's meaning explanations

Talk by Abraham W.

Martin-Löf's meaning explanations provide an approach to understand mathematical statements as statements about functional computer programs. Furthermore, meaning explanations can be used to justify the inference rules of intuitionistic type theory.

As usual, there's mingling at the local bar after the talk.