Skip to main content
PRL Project

The Type Base and Undecidability in Type Theory

by Abhishek Anand

Location: 12:05-1:00, 215 Upson Hall

In this talk, I would talk about the new type Base which was introduced to NUPRL a few years ago. This type contains all the terms of the underlying computation system and equality is based on a notion of observational equivalence. Then, I will show how it let's us express undecidablity in an elegant way. This construction is similar to an earlier construction which was based on bar types. These results prevent us from doing classical logic the way we did earlier - by introducing a "magical" decider for the law of excluded middle. I will show how to get around this problem.