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.

PRL Home
Introduction
The Nuprl book
Origins of the PRL Project
Goals
Dynamics of the Project
Mathematical Expression in Nuprl
Cross Links to Math & CS Fields

Knowledge Base
Math Library
Publications
Projects
CRASH
Nuprl/FDL System
EventML Software
Seminar

People
Wiki
The Book
Lectures
Other Groups

Internalizing proofs and provability

by Aleksey Nogin 2000-2001

by Aleksey Nogin
2000-2001