KnowledgeBase » SEMINAR » ID = 643

Urelements in Computational Type Theory

by Mark Bickford
2004-2005

Set theory with urelements has been used to construct models where the axiom of choice fails. Adding urelements to computational type theory enables several useful applications. We can use them as permutable names, we can use them as "unguessable secrets" to model cryptographic assumptions, and we can use them to name random processes in a theory of independent random sequences.

In this talk I will outline some of these applications and then present the basic primitives that we add to Nuprl to implement the theory.