PRL Seminars

Abstract

I'll show how we can define abstract data structures such as Set and Table in MetaPRL using depnedend records, and implement such structures using binary trees and red-black trees.

I faced some unexpected problems connecting with functionality and recursive types.

It turns out that Nuprl rules for recursive type are invalid and lead to contradiction!