# * Internalizing proofs and provability *

## by Aleksey Nogin

2000-2001

I will present an overview of several approaches for internalizing proofs and provability in Nuprl type theory with and without Term type and Eli's up/down operator.