Kurt Gödel Research Center

2015 seminar talk: Lambda-Calculus and Dependent Type Theory

Talk held by Dana S. Scott (Carnegie Mellon University, Pittsburgh, Pennsylvania, USA and UC Berkeley, California, USA) at the KGRC seminar on 2015-07-02.

Abstract

The speaker has a favorite lambda-calculus model, as he will explain, but he could start with any model and graft on dependent types using partial equivalence relations. The scheme is very simple and leads to a number of good, but elementary exercises in logic. He wishes he had thought of it many years ago.