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.
Lambda-Calculus and Dependent Type Theory
02.07.2015 15:00 - 16:30
Organiser:
KGRC
Location:
SR 101, 2. St., Währinger Str. 25